%\gray
\subsection{Category of Abelian Sheaves}
\begin{definition}
Let $\bcP:\bcC_{\tau}\rightarrow \bcA$ be an $\bcA$-(pre-)sheaf on the site $\bcC$. If $\bcA$ is an abelian category, we say that $\bcP$ is an abelian (pre-)sheaf.
\end{definition}
\begin{theorem}
Let $\bcC_{\tau}$ be a site, $\bcA$ be an abelian category, then $\PreC$ is an abelian category.
\end{theorem}
\begin{proof}
\tcg{??Strightforward application of more general theorem on functors}
\end{proof}
\begin{remark}
In the rest of this \tcb{subsection} $\bcC_{\tau}$ will be a site, $\bcA$ an abelian category, $f:V\rightarrow U$ in $\bcC$, $\bcU'=\{g_j:U'_j\rightarrow U|j\in J\}\stackrel{\phi_{\epsilon}}{\longrightarrow}\bcU=\{f_i:U_i\rightarrow U|i\in I\}$ in $C_U$, $\varphi:\bcP\rightarrow\bcQ$ in $\PreC$, unless mentioned otherwise.
\end{remark}
\subsubsection{Sheafification}\label{Sheafification}
\tcb{type the main result of sheafification.}\\
Let $\goi:\ShvC \rightarrow \PreC$ be the inclusion functor. The aim of the next paragraphs is to construct a left adjoint of $\goi$.
\begin{definition}[$\check{C}$ech Cohomology]\label{H0(-,-)}
We define $$H_U^0(-,-):C_U^{op}\times \PreC\rightarrow \bcA$$
On object by:
$$H_U^0(\bcU,\bcP)=\Ker(\xymatrix{ \displaystyle\prod_{i\in I}\bcP(U_i)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} &&\displaystyle\prod_{i,j\in I}\bcP(U_i\times_U U_j)})$$
And on morphisms by $H_U^0(\phi_{\epsilon},\varphi)$, the unique morphism that makes the following diagram commutative:\\
\begin{equation}\label{H_U^0Summary}
\xymatrix{
\bcP(U)^{\eta_{\bcP,\bcU}}\ar[d]_{\varphi_U}&\bcP_U(\bcU)\ar[rr]^{\ker_{\bcP,\bcU}}\ar@{-->}[dd]_{H_U^0(\phi_{\epsilon},\varphi)}&&
\displaystyle\prod_{k\in I}\bcP(U_k)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} \ar[dd]^{\displaystyle\prod_{l\in J}\varphi_{U'_l}\circ\bcP(\phi_l)}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[dd]^{\displaystyle\prod_{l,l'\in J}\varphi_{U'_l\times_U U'_{l'}}\circ\bcP(\phi_l\times_U\phi_{l'})}&\\
\\
\bcQ(U)\ar[r]^{\eta_{\bcQ,\bcU'}}&\bcQ_U(\bcU')\ar[rr]^{\ker_{\bcQ,\bcU'}}&&
\displaystyle\prod_{l\in J}\bcQ(U'_l)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} &&
\displaystyle\prod_{l,l'\in J}\bcQ(U'_l\times_U U'_{l'})&
}
\end{equation}
The existence of $H_U^0(\phi_{\epsilon},\varphi)$ is due to the universal property of $\bcQ_U(\bcU')$, and the commutativity of the partial right diagrams. That, $\displaystyle\prod_{l\in J}\bcP(\phi_l)$ and $\displaystyle\prod_{l,l'\in J}\bcP(\phi_l\times_U\phi_{l'})$ are the the unique morphisms that make the sides of following two families of 3D-diagrams commutate:$\forall j,j'\in J$
\begin{equation}\label{RefProd}
{\tiny \xymatrix{
\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rr]^{\rho_1}\ar[dr]|{\pi_{\epsilon(j)}} \ar[ddd]|{\displaystyle\prod_{l\in J}\bcP(\phi_l)}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[ddd]|{\displaystyle\prod_{l,l'\in J}\bcP(\phi_l\times_U\phi_{l'})}\ar[dr]|{\pi_{\epsilon(j),\epsilon(j')}}&\\
&\bcP(U_{\epsilon(j)})\ar[d]|{\bcP(\phi_j)}\ar[rr]|{\rho_{1,\epsilon(j),\epsilon(j')}}&&\bcP(U_{\epsilon(j)}\times_U U_{\epsilon(j')})\ar[d]|{\bcP(\phi_j\times_U \phi_{j'})}\\
&\bcP(U'_j)\ar[rr]|{\rho_{1,j,j'}}&&\bcP(U'_j\times_U U'_{j'})\\
\displaystyle\prod_{l\in J}\bcP(U'_j)\ar[rr]_{\rho_1}\ar[ur]|{\pi_j} &&
\displaystyle\prod_{l,l'\in J}\bcP(U'_l\times_U U'_{l'})\ar[ur]|{\pi_{j,j'}}&
} 
\xymatrix{
\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rr]^{\rho_2}\ar[dr]|{\pi_{\epsilon(j')}} \ar[ddd]|{\displaystyle\prod_{l\in J}\bcP(\phi_l)}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[ddd]|{\displaystyle\prod_{l,l'\in J}\bcP(\phi_l\times_U\phi_{l'})}\ar[dr]|{\pi_{\epsilon(j),\epsilon(j')}}&\\
&\bcP(U_{\epsilon(j')})\ar[d]|{\bcP(\phi_{j'})}\ar[rr]|{\rho_{2,\epsilon(j),\epsilon(j')}}&&\bcP(U_{\epsilon(j)}\times_U U_{\epsilon(j')})\ar[d]|{\bcP(\phi_j\times_U \phi_{j'})}\\
&\bcP(U'_{j'})\ar[rr]|{\rho_{2,j,j'}}&&\bcP(U'_j\times_U U'_{j'})\\
\displaystyle\prod_{l\in J}\bcP(U'_j)\ar[rr]_{\rho_2}\ar[ur]|{\pi_{j'}} &&
\displaystyle\prod_{l,l'\in J}\bcP(U'_l\times_U U'_{l'})\ar[ur]|{\pi_{j,j'}}&
}}
\end{equation}
Such morphisms exists by and universal property of product. That, definitions of \tcg{$\phi_j\times_U \phi_{j'}$}, $\rho_1$, and $\rho_2$ guarantee the commutativity of the front face. Then, straight forward calculations shows the commutativity of the back square. That implies the commutativity of the upper right square in \ref{H_U^0_1}, which in turn implies the existence of the unique $H_U^0(\phi_{\epsilon},id_{\bcP})$ that makes upper left square in \ref{H_U^0_1} commutate.\\
And, $\displaystyle\prod_{l\in J}\varphi_{U'_l}$ and $\displaystyle\prod_{l,l'\in J}\varphi_{U'_l\times_U U'_{l'}}$ are the the unique morphisms that make the sides of following two families of 3D-diagrams commutate:$\forall j,j'\in J$
$$
{\tiny \xymatrix{
\displaystyle\prod_{l\in J}\bcP(U'_l)\ar[rr]^{\rho_1}\ar[dr]|{\pi_j} \ar[ddd]|{\displaystyle\prod_{l\in J}\varphi_{U'_l}}&&
\displaystyle\prod_{l,l'\in J}\bcP(U'_l\times_U U'_{l'})\ar[ddd]|{\displaystyle\prod_{l,l'\in J}\varphi_{U'_l\times_U U'_{l'}}}\ar[dr]|{\pi_{j,j'}}&\\
&\bcP(U'_j)\ar[d]|{\varphi_{U'_j}}\ar[rr]|{\rho_{1,j,j'}}&&\bcP(U'_j\times_U U'_{j'})\ar[d]|{\varphi_{U'_j\times_U U'_{j'}}}\\
&\bcQ(U'_j)\ar[rr]|{\rho_{1,j,j'}}&&\bcQ(U'_j\times_U U'_{j'})\\
\displaystyle\prod_{l\in J}\bcQ(U'_j)\ar[rr]_{\rho_1}\ar[ur]|{\pi_j} &&
\displaystyle\prod_{l,l'\in I}\bcQ(U'_j\times_U U'_{j'})\ar[ur]|{\pi_{j,j'}}&
} \xymatrix{
\displaystyle\prod_{l\in J}\bcP(U'_l)\ar[rr]^{\rho_2}\ar[dr]|{\pi_{j'}} \ar[ddd]|{\displaystyle\prod_{l\in J}\varphi_{U'_l}}&&
\displaystyle\prod_{l,l'\in J}\bcP(U'_l\times_U U'_{l'})\ar[ddd]|{\displaystyle\prod_{l,l'\in J}\varphi_{U'_l\times_U U'_{l'}}}\ar[dr]|{\pi_{j,j'}}&\\
&\bcP(U'_j)\ar[d]|{\varphi_{U'_{j'}}}\ar[rr]|{\rho_{2,j,j'}}&&\bcP(U'_j\times_U U'_{j'})\ar[d]|{\varphi_{U'_j\times_U U'_{j'}}}\\
&\bcQ(U'_{j'})\ar[rr]|{\rho_{2,j,j'}}&&\bcQ(U'_j\times_U U'_{j'})\\
\displaystyle\prod_{l\in J}\bcQ(U'_j)\ar[rr]_{\rho_2}\ar[ur]|{\pi_{j'}} &&
\displaystyle\prod_{l,l'\in I}\bcQ(U'_j\times_U U'_{j'})\ar[ur]|{\pi_{j,j'}}&
}}
$$
Such morphisms exists by and universal property of product. That, the naturality of $\varphi$, and definition of $\rho_1,\rho_2$ guarantees the commutativity of the front face. Then, straight forward calculations shows the commutativity of the back square. That implies the commutativity of the lower right square in \ref{H_U^0_1}, which in turn implies the existence of the unique $H_U^0(id_{\bcU'},\varphi)$ that makes lower left square in \ref{H_U^0_1} commutate.\\
\tcg{prove the commutativity of the left hand side. Also, add the missing bits to the small diagrams} Hence, \eqref{H_U^0Summary} commute.\\
Since $H_U^0(id_{\bcU'},\varphi)$ and $H_U^0(\phi_{\epsilon},id_{\bcP})$ are the unique morphisms that make the following diagram commute:
\begin{equation}\label{H_U^0_1}
\xymatrix{
\bcP_U(\bcU)\ar[rr]^{\ker_{\bcP,\bcU}}\ar@{-->}[dd]|=_{H_U^0(\phi_{\epsilon},id_{\bcP})}^{\bcP_U(\phi_{\epsilon})}&&
\displaystyle\prod_{k\in I}\bcP(U_k)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} \ar[dd]^{\displaystyle\prod_{l\in J}\bcP(\phi_l)}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[dd]^{\displaystyle\prod_{l,l'\in J}\bcP(\phi_l\times_U\phi_{l'})}&\\
\\
\bcP_U(\bcU')\ar[rr]^{\ker_{\bcP,\bcU'}}\ar@{-->}[dd]_{H_U^0(id_{\bcU'},\varphi)}|=^{\varphi_{\bcU'}}&&
\displaystyle\prod_{l\in J}\bcP(U'_l)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} \ar[dd]^{\displaystyle\prod_{l\in J}\varphi_{U'_l}}&&
\displaystyle\prod_{l,l'\in J}\bcP(U'_l\times_U U'_{l'})\ar[dd]^{\displaystyle\prod_{l,l'\in J}\varphi_{U'_l\times_U U'_{l'}}}&\\
\\
\bcQ_U(\bcU')\ar[rr]^{\ker_{\bcQ,\bcU'}}&&
\displaystyle\prod_{l\in J}\bcQ(U'_l)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} &&
\displaystyle\prod_{l,l'\in J}\bcQ(U'_l\times_U U'_{l'})&
}
\end{equation}
Then, $H_U^0(\phi_{\epsilon},\varphi)= H_U^0(id_{\bcU'},\varphi)\circ H_U^0(\phi_{\epsilon},id_{\bcP})$.\\
On the other hand, since $\varphi:\bcP\rightarrow \bcQ$ is morphism of pre-sheaves, i.e. a natural transformation, we have\\
$$\varphi_{U'_l}\circ \bcP(\phi_l)= \bcQ(\phi_l)\circ\varphi_{U_l}, \forall l\in J\  \Rightarrow$$
$${\displaystyle\prod_{l\in J}\varphi_{U'_l}\circ\bcP(\phi_l)}={\displaystyle\prod_{l\in J}\bcQ(\phi_l)\circ\varphi_{U_l}}$$
$$\varphi_{U'_l\times_U U'_{l'}}\circ \bcP(\phi_l\times_U\phi_{l'})= \bcQ(\phi_l\times_U\phi_{l'})\circ\varphi_{U'_l\times_U U'_{l'}}, \forall l,l'\in J\  \Rightarrow$$
$${\displaystyle\prod_{l,l'\in J}\varphi_{U'_l\times_U U'_{l'}}\circ\bcP(\phi_l\times_U\phi_{l'})}={\displaystyle\prod_{l,l'\in J}\bcQ(\phi_l\times_U\phi_{l'})\circ\varphi_{U'_l\times_U U'_{l'}}}$$
Therefore, 
$H_U^0(\phi_{\epsilon},\varphi)= H_U^0(\phi_{\epsilon},id_{\bcQ}) \circ H_U^0(id_{\bcU},\varphi)$.\\
That, $H_U^0(\phi_{\epsilon},id_{\bcQ}) $ and $ H_U^0(id_{\bcU},\varphi)$ are the 
the unique morphisms that make the following diagram commute:
\begin{equation}\label{H_U^0_2}
\xymatrix{
\bcP_U(\bcU)\ar[rr]^{\ker_{\bcP,\bcU}}\ar@{-->}[dd]_{H_U^0(id_{\bcU},\varphi)}|=^{\varphi_{\bcU}}&&
\displaystyle\prod_{k\in I}\bcP(U_k)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} \ar[dd]^{\displaystyle\prod_{l\in J}\varphi_{U_l}}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[dd]^{\displaystyle\prod_{l,l'\in J}\varphi_{U_l\times_U U_{l'}}}&\\
\\
\bcQ_U(\bcU)\ar[rr]^{\ker_{\bcQ,\bcU}}\ar@{-->}[dd]|=_{H_U^0(\phi_{\epsilon},id_{\bcQ})}^{\bcQ_{U}(\phi_{\epsilon})}&&
\displaystyle\prod_{l\in J}\bcQ(U_l)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} \ar[dd]^{\displaystyle\prod_{l\in J}\bcQ(\phi_l)}&&
\displaystyle\prod_{l,l'\in J}\bcQ(U_l\times_U U_{l'})\ar[dd]^{\displaystyle\prod_{l,l'\in J}\bcQ(\phi_l\times_U\phi_{l'})}&\\
\\
\bcQ_U(\bcU')\ar[rr]^{\ker_{\bcQ,\bcU'}}&&
\displaystyle\prod_{l\in J}\bcQ(U'_l)\ar@<-3pt>[rr]_{\rho_2}\ar@<3pt>[rr]^{\rho_1} &&
\displaystyle\prod_{l,l'\in J}\bcQ(U'_l\times_U U'_{l'})&
}
\end{equation}
\end{definition}
\begin{remark}
\tcb{The aim of sheafification is to obtain a sheaf starting from a pre-sheaf. Since the condition of the sheaf is the exactness of \ref{sheaf}. Then, it is natural to start with defining objects that makes \ref{sheaf}-like diagram exact.}
\end{remark}
\begin{remark}
Above defined $H_U^0(-,-)$ is a bi-functor, that it's well-defined as $\Ker$ exist in $\bcA$, and being defined on morphisms using the universal property of $\Ker$ guarantees the satisfaction of composition and identity axioms. Hence, $H_U^0(-,\bcP):C_U^{op}\rightarrow \bcA$ is also a functor, $\forall \bcP \in \PreC$, called the section functor. 
\end{remark}
\begin{remark}
\tcb{The above notation $H_U^0(-,-)$ is used to emphasise that it is a cohomology of dimension zero}. However, in the sheafification, we will not be using cohomology of higher dimensions. Therefore, we will use the notation: $\bcP_U(-):=H_U^0(-,\bcP)$, $\forall \bcP \in \PreC$.
\end{remark}
\begin{lemma}\label{NT_U}
The collection $\varphi_U:=\{\varphi_U(\bcU)|\bcU\in C_U\}$ defines a natural transformation $\varphi_U:\bcP_U\rightarrow\bcQ_U$ that $\varphi_U(\bcU')\circ \bcP_U((\epsilon,\phi))=H^0_U((\epsilon,\phi),\varphi)= \bcQ_U((\epsilon,\phi))\circ\varphi_U(\bcU)$, using \eqref{H_U^0_1} and \eqref{H_U^0_2}.
\end{lemma}
\begin{remark}
$\rho_{1,\bcU}\circ \rho_{\bcU}=\rho_{2,\bcU}\circ \rho_{\bcU}$. Hence, $\exists!\eta_{\bcU}:\bcP(U)\rightarrow \bcP_U(\bcU)$ that makes the following diagram commute:
$$
\xymatrix{
\bcP_U(\bcU)\ar[rr]^{\ker_{\bcP,\bcU}}&&\displaystyle\prod_{k\in I}\bcP(U_k)\\
\bcP(U)\ar@{-->}[u]^{\eta_{\bcU}}\ar[rru]_{\rho_{\bcU}}}
$$
\begin{equation}\label{kerU}
\ker_{\bcP,\bcU}\circ \eta_{\bcU}=\rho_{\bcU}
\end{equation}
\end{remark}
\begin{lemma}\label{CovPro}
Let $\phi_{\epsilon},\psi_{\delta}:\bcU'\rightarrow \bcU$ be refinement morphisms, then $\bcP_U(\phi_{\epsilon})=\bcP_U(\psi_{\delta})$
\end{lemma}
\begin{proof}
$\forall j\in J$, define $\Delta_j:U'_j\rightarrow U_{\epsilon(j)\times_U\delta(j)}$ to be the unique morphism that makes the following diagram commute:
$$
\xymatrix{&&&U_{\epsilon(j)}\ar[rd]^{f_{\epsilon(j)}}&\\
U'_j\ar@/^/[rrru]^{\phi_j}\ar@/_/[rrrd]_{\psi_j}\ar@{-->}[rr]|{\Delta_j}&&U_{\epsilon(j)}\times_UU_{\delta(j)}\ar[ru]|{p_{1,\epsilon(j),\delta(j)}}\ar[rd]|{p_{2,\epsilon(j),\delta(j)}}&&U\\
&&&U_{\delta(j)}\ar[ru]_{f_{\delta(j)}}&
}
$$
That $f_{\epsilon(j)}\circ\phi_j=g_j=f_{\delta(j)}\circ\psi_j$. Then, consider the following composition of commutative diagram:
$$
{\tiny \xymatrix{
\bcP_U(\bcU)\ar[ddddd]_{\bcP_U(\phi_{\epsilon})}\ar[r]^{\ker_{\bcP,\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rrrrr]^{\rho_1}\ar[dr]|{\pi_{\epsilon(j)}} \ar[dddd]|{\displaystyle\prod_{l\in J}\bcP(\phi_l)}&&&&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[dl]|{\pi_{\epsilon(j),\delta(j)}}\\
&&\bcP(U_{\epsilon(j)})\ar[dd]|{\bcP(\phi_j)}\ar[rrr]|{\rho_{1,\epsilon(j),\delta(j)}}&&&\bcP(U_{\epsilon(j)}\times_U U_{\delta(j)})\ar[ddlll]|{\bcP(\Delta_j)}&\\
&&&&&&\\
&&\bcP(U'_j)&&&\bcP(U_{\delta(j)})\ar[lll]|{\bcP(\psi_j)}\ar[uu]|{\rho_{2,\epsilon(j),\delta(j)}}&\\
&\displaystyle\prod_{l\in J}\bcP(U'_j)\ar[ru]|{\pi_j} &&&&&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[uuuu]_	{\rho_2}\ar[ul]|{\pi_{\delta(j)}} \ar[lllll]|{\displaystyle\prod_{l\in J}\bcP(\psi_l)}\\
\bcP_U(\bcU')\ar[ur]|{\ker_{\bcP,\bcU'}}&&&&&&\bcP_U(\bcU')\ar[llllll]^{\bcP_U(\psi_{\delta})}\ar[u]_{\ker_{\bcP,\bcU}}
}} 
$$
%$${\small \xymatrix{\bcP_U(\bcU)\ar[ddd]_{\bcP_U(\phi_{\epsilon})}\ar[r]^{\ker_{\bcP,\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rrrr]^{\rho_1}\ar[dr]|{\pi_{\epsilon(j)}} \ar[ddd]|{\displaystyle\prod_{l\in J}\bcP(\phi_l)}&&&&\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[d]|{\pi_{\epsilon(j),\delta(j)}}\\&&\bcP(U_{\epsilon(j)})\ar[dd]|{\bcP(\phi_j)}\ar[rrr]|{\rho_{1,\epsilon(j),\delta(j)}}&&&\bcP(U_{\epsilon(j)}\times_U U_{\delta(j)})\ar[ddlll]^{\bcP(\Delta_j)}\\&&&&&\\\bcP_U(\bcU')\ar[r]_{\ker_{\bcP,\bcU'}}&\displaystyle\prod_{l\in J}\bcP(U'_j)\ar[r]_{\pi_j} &\bcP(U'_j)&&&}} $$
%Which implies that:$\pi_j\circ \ker_{\bcP,\bcU'}\circ\bcP_U(\phi_{\epsilon})=\bcP(\Delta_j)\circ\pi_{\epsilon(j),\delta(j)}\circ \rho_1\circ \ker_{\bcP,\bcU}$
%$${\small \xymatrix{\bcP_U(\bcU)\ar[ddd]_{\bcP_U(\psi_{\delta})}\ar[r]^{\ker_{\bcP,\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rrrr]^{\rho_2}\ar[dr]|{\pi_{\delta(j)}} \ar[ddd]|{\displaystyle\prod_{l\in J}\bcP(\psi_l)}&&&&\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[d]|{\pi_{\delta(j),\delta(j)}}\\&&\bcP(U_{\delta(j)})\ar[dd]|{\bcP(\psi_j)}\ar[rrr]|{\rho_{2,\delta(j),\delta(j)}}&&&\bcP(U_{\epsilon(j)}\times_U U_{\delta(j)})\ar[ddlll]^{\bcP(\Delta_j)}\\&&&&&\\\bcP_U(\bcU')\ar[r]_{\ker_{\bcP,\bcU'}}&\displaystyle\prod_{l\in J}\bcP(U'_j)\ar[r]_{\pi_j} &\bcP(U'_j)&&&}} $$
%Which implies that: $\pi_j\circ \ker_{\bcP,\bcU'}\circ\bcP_U(\psi_{\delta})=\bcP(\Delta_j)\circ\pi_{\epsilon(j),\delta(j)}\circ \rho_2\circ \ker_{\bcP,\bcU}$\\\\
That implies:\\
$\pi_j\circ \ker_{\bcP,\bcU'}\circ\bcP_U(\phi_{\epsilon})=\bcP(\Delta_j)\circ\pi_{\epsilon(j),\delta(j)}\circ \rho_1\circ \ker_{\bcP,\bcU}$\\
$\pi_j\circ \ker_{\bcP,\bcU'}\circ\bcP_U(\psi_{\delta})=\bcP(\Delta_j)\circ\pi_{\epsilon(j),\delta(j)}\circ \rho_2\circ \ker_{\bcP,\bcU}$\\\\
Notice that $\rho_1\circ \ker_{\bcP,\bcU}=\rho_2\circ \ker_{\bcP,\bcU}$. Hence,
$$\pi_j\circ \ker_{\bcP,\bcU'}\circ\bcP_U(\psi_{\delta})=\pi_j\circ \ker_{\bcP,\bcU'}\circ\bcP_U(\phi_{\epsilon}),\forall j\in J$$.
Then, the universal property of $\displaystyle\prod_{l\in J}\bcP(U'_j)$ implies that $\ker_{\bcP,\bcU'}\circ\bcP_U(\psi_{\delta})=\ker_{\bcP,\bcU'}\circ\bcP_U(\phi_{\epsilon})$. Since $\ker_{\bcP,\bcU'}$ is a monomorphism, then $\bcP_U(\psi_{\delta})=\bcP_U(\phi_{\epsilon})$.
\end{proof}
Since the refinement morphisms agrees on the level of cohomology, that motivate the below definition:
\begin{definition}
We define the category $\Cov(U)$ to be the category with objects $CoU'_{\tau}(U)$, and a unique morphism $\bcU'\rightarrow \bcU$ if there exists a refinement morphism $\bcU'\rightarrow \bcU$.
\end{definition}
\begin{remark}
Abusing the notation, one can find readily that$\bcP_U:\Cov(U)^{op}\rightarrow \bcA$ defines a functor by sending $\bcU$ to above defined $\bcP_U(\bcU)$, and the unique morphism $\bcU'\rightarrow \bcU$ to $\bcP_U(\phi_{\epsilon})$, for any refinement morphism $\phi_{\epsilon}:\bcU'\rightarrow \bcU$.
\end{remark}

\tcb{What about $\displaystyle\prod_{l\in J}\bcP(\phi_l)$ and $\displaystyle\prod_{l\in J}\bcP(\psi_l)$? Would they be equal? Either prove, or give a counter example. Most likely, counter example}
\begin{lemma}\label{RhoUPhiV}
$\rho_{\bcU'}=\displaystyle\prod_{l\in J}\bcP(\phi_l)\circ \rho_{\bcU}$, i.e. the following diagram commutes:
$$
\xymatrix{\bcP(U)\ar[r]^{\rho_{\bcU}}\ar[rd]_{\rho_{\bcU'}}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[d]^{\displaystyle\prod_{l\in J}\bcP(\phi_l)}\\
& \displaystyle\prod_{l\in J}\bcP(U'_l)}
$$
\end{lemma}
\begin{proof}
$\forall j\in J$, consider the diagram:
$$
\xymatrix{\bcP(U) \ar[ddd]_{\rho_{\bcU}}\ar[ddddr]|{\rho_{\bcU'}}\ar[ddddrrr]|{\bcP(g_j)}\ar[dddrr]^{\bcP(f_{\epsilon(j)})}&&&\\
\\
\\
\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rr]|{\pi_{\epsilon(j)}}\ar[rd]_{\displaystyle\prod_{l\in J}\bcP(\phi_l)}&&\bcP(U_{\epsilon(j)})\ar[rd]^{\bcP(\phi_j)}&\\
&\displaystyle\prod_{l\in J}\bcP(U'_l)\ar[rr]|{\pi_j}&&\bcP(U'_j)
}
$$
We notice that front and back diagrams commute by the definition of $\rho$, the right-side diagram commutes by the definition of refinement morphism, and the bottom diagram commutes by the definition of $\displaystyle\prod_{l\in J}\bcP(\phi_l)$. Then, we have\\
 $\pi_j\circ \rho_{\bcU'}=\bcP(g_j)=\bcP(\phi_j)\circ \bcP(f_{\epsilon(j)})=\bcP(\phi_j)\circ \pi_{\epsilon(j)}\circ \rho_{\bcU}=\pi_j\circ \displaystyle\prod_{l\in J}\bcP(\phi_l) \circ \rho_{\bcU}$.\\
Then, by the universal property of $\displaystyle\prod_{l\in J}\bcP(U'_l)$, we have\\
$\rho_{\bcU'} =\displaystyle\prod_{l\in J}\bcP(\phi_l) \circ \rho_{\bcU}$.
\end{proof}
\begin{lemma}\label{kPPhik}
$\eta_{\bcU'}=\bcP_U(\phi_{\epsilon})\circ \eta_{\bcU}$, i.e. the following diagram commutes:
$$
\xymatrix{\bcP(U)\ar[r]^{\eta_{\bcU}}\ar[rd]_{\eta_{\bcU'}}&\bcP_U(\bcU)\ar[d]^{\bcP_U(\phi_{\epsilon})}\\
&\bcP_U(\bcU')}
$$
\end{lemma}
\begin{proof}Consider the diagram
$$
\xymatrix{
\bcP(U)\ar[r]^{\eta_{\bcU}}\ar[rdd]_{\eta_{\bcU'}}&\bcP_U(\bcU)\ar[rr]^{\ker_{\bcP,\bcU}}\ar[dd]^{\bcP_U(\phi_{\epsilon})}&&
\displaystyle\prod_{k\in I}\bcP(U_k)\ar[dd]^{\displaystyle\prod_{l\in J}\bcP(\phi_l)}\\
\\
&\bcP_U(\bcU')\ar[rr]^{\ker_{\bcP,\bcU'}}&&\displaystyle\prod_{l\in J}\bcP(U'_l)}
$$
We notice that \ref{kerU} and \ref{RhoUPhiV} imply the commutativity of the \tcr{external} diagram, and \ref{H_U^0_1} implies the commutativity of the inner square diagram. Hence, \\
$\ker_{\bcP,\bcU'}\circ \eta_{\bcU'}={\displaystyle\prod_{l\in J}\bcP(\phi_l)}\circ\ker_{\bcP,\bcU}\circ \eta_{\bcU}= \ker_{\bcP,\bcU'}\circ \bcP_U(\phi_{\epsilon}) \circ \eta_{\bcU}$.\\
Notice that $\ker_{\bcP,\bcU'}$ is a monomorphism. Hence, $\eta_{\bcU'}=\bcP_U(\phi_{\epsilon}) \circ \eta_{\bcU}$
\end{proof}



\tcg{Type schemes examples of this construction}\\
\tcg{Try to explain that this definition is natural!}\\
\tcg{Try to explain seprability}\\
\begin{lemma}\label{fastphiL}
$f$ and $\phi_{\epsilon}$ induce a canonical refinement morphism $f^{\ast}\phi_{\epsilon}:f^{\ast}\bcU'\rightarrow f^{\ast}\bcU$
\end{lemma}
\begin{proof}
Define $f^{\ast}\phi_{\epsilon}:=(\epsilon, \{f^{\ast}\phi_j|j\in J\})$, where $f^{\ast}\phi_j$ the unique morphism - induced by the universal property of $U_{\epsilon(j)}\times_U V$ - that makes the following 3D-diagram commute:
%$${\xymatrix{U'_j\ar[rr]^{\phi_j}\ar[rdd]|{g_j}&&U_{\epsilon(j)}\ar[ddl]|{f_{\epsilon(j)}}&&&\\\\&U&&&&\\&&&U'_j\times_U V\ar@{-->}[rr]^{f^{\ast}\phi_j}\ar[rdd]|{p_{2,U'_j,V}}\ar[uuulll]|{p_{1,U'_j,V}}&&U_{\epsilon(j)}\times_U V\ar[ddl]|{p_{2,U_{\epsilon(j)},V}}\ar[uuulll]|{p_{1,U_{\epsilon(j)},V}}\\\\&&&&V\ar[uuulll]|f&}}$$
\begin{equation}\label{fastphi}
\xymatrix{
U'_j\times_U V\ar@{-->}[dd]_{f^{\ast}\phi_j}\ar[dr]|{p_{2,U'_j,V}}\ar[rrrr]|{p_{1,U'_j,V}} &&&& U'_j\ar[rd]|{g_j}\ar[dd]|{\phi_j}&\\
&V\ar[rrrr]|f|!{"2,2";"2,5"}{\hole\hole\hole\hole}&&&&U\\
U_{\epsilon(j)}\times_U V\ar[ur]|{p_{2,U_{\epsilon(j)},V}}\ar[rrrr]|{p_{1,U_{\epsilon(j)},V}} &&&& U_{\epsilon(j)}\ar[ru]|{f_{\epsilon(j)}}&
}
\end{equation}
That, the upper and right side diagrams are commutative. Then, the commutativity of the 3D-diagram (particularly of the left side diagram)implies that $f^{\ast}\phi_{\epsilon}:f^{\ast}\bcU'\rightarrow f^{\ast}\bcU$ is a refinement morphism.
\end{proof}
\begin{lemma}
$f$ induce a canonical functor $\hat{f}^{\ast}:C_U\rightarrow C_V$
\end{lemma}
\begin{proof}
Let $\hat{f}^{\ast}(\bcU)=f^{\ast}(\bcU)$, $\hat{f}^{\ast}(\phi_{\epsilon})=f^{\ast}\phi_{\epsilon}$. Since, $f^{\ast}\phi_{\epsilon}$ is defined by universal property, then straightforward calculations shows that $\hat{f}^{\ast}$ is a functor.
\end{proof}
\tcb{Any special property for this functor?}\\
\tcb{Check if $\hat{-}^{\ast}:\bcC^{op}\rightarrow $ Category of categories of covering, is a functor, no, but show the isomorphism}\\
\tcb{Was it enough to consider it on $\Cov$'s}



\begin{lemma}
Let $f:V\rightarrow U$, $g:W\rightarrow V$ in $\bcC$, then $\hat{g}^{\ast}\circ \hat{f}^{\ast}$ is naturally \tcr{isomorphic} to $\widehat{f\circ g}^{\ast}$.
\end{lemma}
\begin{proof}
Define $n_{\bcU}:=(id_I,\{n_{\bcU,i}|i\in I\})$, where $n_{\bcU,i}$ is defined to be the unique morphism that makes the following diagram commute, $\forall i \in I$:
\begin{equation}
\label{nU}
{\small \xymatrix{
(U_i\times_U W)\ar@/^/[rrrrrd]^{p_{1,U_i,W}}\ar@/_/[rdd]_{p_{2,U_i,W}}&&&&&\\
&(U_i\times_U V)\times_V W\ar@{-->}[ul]|{n_{\bcU,i}} \ar[rr]_{p_{1,U_i\times_U V,W}}\ar[d]|{p_{2,U_i\times_U V,W}}&&U_i\times_U V\ar[rr]_{p_{1,U_i,V}}\ar[d]|{p_{2,U_i,V}}&&U_i\ar[d]^{f_i}\\
&W\ar[rr]_g&&V\ar[rr]_f&&U
}}
\end{equation}
Hence, $n_{\bcU}:\hat{g}^{\ast}\circ \hat{f}^{\ast}(\bcU)\rightarrow  \widehat{f\circ g}^{\ast}(\bcU)$ is a refinement morphism.\\
Notice that the collection $\{n_{\bcU}|\bcU\in C_U\}$ defines a natural transformation:
$$n:\hat{g}^{\ast}\circ \hat{f}^{\ast}\stackrel{\cdot}{\rightarrow}  \widehat{f\circ g}^{\ast}$$
That, the following diagram commutes, $\forall \phi_{\epsilon}:\bcU'\rightarrow \bcU$ in $C_{U}$:
$$
\xymatrix{
\hat{g}^{\ast}\circ \hat{f}^{\ast}(\bcU')\ar[dd]_{\hat{g}^{\ast}\circ \hat{f}^{\ast}(\phi_{\epsilon} )} \ar[rr]^{n_{\bcU'}}&&  \widehat{f\circ g}^{\ast}(\bcU')\ar[dd]^{ \widehat{f\circ g}^{\ast}(\phi_{\epsilon})}\\
\\
\hat{g}^{\ast}\circ \hat{f}^{\ast}(\bcU)\ar[rr]_{n_{\bcU}}&&  \widehat{f\circ g}^{\ast}(\bcU)\\
}
$$
The commutativity of the the above diagram is due to:\\
On the one hand $\epsilon\circ id_{I'}=id_I\circ \epsilon$.
On the other hand, consider the following commutative 3D-diagram, for being a composition of the commutative diagrams \ref{fastphi} and \ref{nU}:
$$
{\small \xymatrix{
U'_{i'}\times_U W\ar@/^/[rrrrrd]|{p_{1}}\ar@{..>}@/_/[rrdd]\ar@/_/[dddd]|{(f\circ g)^{\ast}\phi_{i'}}&&&&&\\
&\tiny{(U'_{i'}\times_U V)\times_V W}\ar[ul]|{n_{\bcU',{i'}}} \ar[rr]|{p_{1}}\ar[rd]|{p_{2}}  \ar@/_/[dd]|{g^{\ast}f^{\ast}\phi_{i'}}   &&U'_{i'}\times_U V  \ar@/_/[dd]|{f^{\ast}\phi_{i'}}   \ar[rr]|{p_{1}}\ar[rd]|{p_{2}}&&U'_{i'}\ar[rd]^{f_{i'}}\ar@/_/[dd]|{\phi_{i'}}\\
&&W\ar@{..>}[rr]|{\hole\hole\hole\hole g}&&V\ar@{..>}[rr]|{\hole\hole\hole f}&&U\\
&\tiny{(U_{\epsilon(i')}\times_U V)\times_V W}\ar[dl]|{n_{\bcU,\epsilon(i')}} \ar[rr]|{p_{1}}\ar[ru]|{p_{2}}&&U_{\epsilon(i')}\times_U V\ar[rr]|{p_{1}}\ar[ru]|{p_{2}}&&U_{\epsilon(i')}\ar[ru]_{f_{\epsilon(i')}}\\
U_{\epsilon(i')}\times_U W\ar@/_/[rrrrru]|{p_{1}}\ar@{..>}@/^/[rruu]&&&&&\\
}}
$$
\tcb{Notice that some of the morphisms names have been shorten, others omitted , in order to make the diagram more readable. Refer to \ref{fastphi} and \ref{nU}, if it causes an ambiguity.}\\
Hence:
$$\small{p_{2,U_{\epsilon(i')},W} \circ (f\circ g)^{\ast}\phi_{i'}\circ n_{\bcU',i'}=p_{2,U'_{i'}\times_U V,W} =p_{2,U_{\epsilon(i')},W} \circ  n_{\bcU,\epsilon(i')}\circ g^{\ast}f^{\ast}\phi_{i'}}$$
$$\small{p_{1,U_{\epsilon(i')},W} \circ (f\circ g)^{\ast}\phi_{i'}\circ n_{\bcU',i'}=
\phi_{i'}\circ p_{1,U'_{i'},V}\circ p_{1,U'_{i'}\times_U V,W} =p_{1,U_{\epsilon(i')},W} \circ  n_{\bcU,\epsilon(i')}\circ g^{\ast}f^{\ast}\phi_{i'}}$$
Therefore, the universal property of $U_{\epsilon(i')}\times_U W$ implies that 
$$(f\circ g)^{\ast}\phi_{i'}\circ n_{\bcU',i'}=  n_{\bcU,\epsilon(i')}\circ g^{\ast}f^{\ast}\phi_{i'}$$
\tcr{Levine claimes on P132 that it is a natural isomorphism, but it it does not seem to be!}
\end{proof}


\begin{lemma}\label{RefDiffObj}
There exist a canonical morphism $\bcP_f(\bcU):\bcP_U(\bcU)\rightarrow \bcP_V(f^{\ast}\bcU)$ that makes the following diagram commute:
$$
\xymatrix{\bcP(U)\ar[d]_{\bcP(f)}\ar[r]^{\eta_{\bcU}}&\bcP_U(\bcU)\ar[d]^{\bcP_f(\bcU)}\ar[r]^{\ker_{\bcP,\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[d]^{\displaystyle\prod_{k\in I}(\bcP(p_{1,U_k,V}))}\\
P(V)\ar[r]^{\eta_{f^{\ast}\bcU}}&\bcP_V(f^{\ast}\bcU)\ar[r]_{\ker_{\bcP,f^{\ast}\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k\times_U V)
}
$$
\end{lemma}
\begin{proof}
Consider the diagram\\
\begin{equation}\label{Co}
{\small
\xymatrix{\bcP(U)\ar[d]_{\bcP(f)}\ar[r]^{\eta_{\bcU}}&\bcP_U(\bcU)\ar@{-->}[d]^{\bcP_f(\bcU)}\ar[r]^{\ker_{\bcP,\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar@<+3pt>[rr]^{\rho_1} \ar@<-3pt>[rr]_{\rho_2}\ar[d]^{\displaystyle\prod_{k\in I}(\bcP(p_{1,U_k,V}))}&&\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[d]^{\displaystyle\prod_{k,k'\in I}(\bcP(p_{1,U_k,V}\times_f p_{1,U_{k'},V}))} \\
P(V)\ar[r]_{\eta_{f^{\ast}\bcU}}&\bcP_V(f^{\ast}\bcU)\ar[r]_{\ker_{\bcP,f^{\ast}\bcU}}&\displaystyle\prod_{k\in I}\bcP(U_k\times_U V)\ar@<+3pt>[rr]^{\rho_1} \ar@<-3pt>[rr]_{\rho_2}&&\displaystyle\prod_{k,k'\in I}\bcP((U_k\times_U V) \times_V (U_{k'}\times_U V)) 
}}
\end{equation}
Where, $\displaystyle\prod_{k\in I}(\bcP(p_{1,U_k,V}))$ and ${\displaystyle\prod_{k,k'\in I}(\bcP(p_{1,U_k,V}\times_f p_{1,U_{k'},V}))}$ are the the unique morphisms that make the sides of following two families of 3D-diagrams commutate:$\forall i,i'\in I$
\begin{equation}\label{CoDetailes}
{\tiny \xymatrix{
\bcP(U)\ar[r]^{\eta_{\bcU}}\ar[rrd]|{\bcP(f_i)}\ar[ddd]_{P(f)}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rr]^{\rho_1}\ar[dr]|{\pi_i} \ar@{..>}[ddd]|{\displaystyle\prod_{k\in I}\bcP(p_{1,U_k,V})}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar[ddd]|{\displaystyle\prod_{k,k'\in I}\bcP(p_{1,U_k,V}\times_f p_{1,U_{k'},V})}\ar[dr]|{\pi_{i,i'}}&\\
&&\bcP(U_i)\ar[d]|{\bcP(p_{1,U_i,V})}\ar[rr]|{\rho_{1,i,i'}}&&\bcP(U_{i}\times_U U_{i'})\ar[d]|{\bcP(p_{1,U_{i},V}\times_f p_{1,U_{i'},V})}\\
&&\bcP(U_i\times_U V)\ar[rr]|{\rho_{1,i,i'}}&&\bcP((U_i\times_U V)\times_V (U_{i'}\times_U V))\\
\bcP(U)\ar[r]_{\eta_{f^{\ast}\bcU}}\ar[rru]|{\bcP(p_{2,U_i,V})}&\displaystyle\prod_{k\in I}\bcP(U_k\times_U V)\ar[rr]_{\rho_1}\ar[ur]|{\pi_i} &&
\displaystyle\prod_{k,k'\in I}\bcP((U_k\times_U V)\times_V (U_{k'}\times_U V))\ar[ur]|{\pi_{i,i'}}&
} 
}
\end{equation}
\begin{equation}
{\tiny \xymatrix{
\bcP(U)\ar[r]^{\eta_{\bcU}}\ar[rrd]|{\bcP(f_i)}\ar[ddd]_{P(f)}&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rr]^{\rho_2}\ar[dr]|{\pi_{i'}} \ar@{..>}[ddd]|{\displaystyle\prod_{k\in I}\bcP(p_{1,U_k,V})}&&
\displaystyle\prod_{k,k'\in I}\bcP(U_k\times_U U_{k'})\ar@{..>}[ddd]|{\displaystyle\prod_{k,k'\in I}\bcP(p_{1,U_k,V}\times_f p_{1,U_{k'},V})}\ar[dr]|{\pi_{i,i'}}&\\
&&\bcP(U_{i'})\ar[d]|{\bcP(p_{1,U_{i'},V})}\ar[rr]|{\rho_{2,i,i'}}&&\bcP(U_{i}\times_U U_{i'})\ar[d]|{\bcP(p_{1,U_{i},V}\times_f p_{1,U_{i'},V})}\\
&&\bcP(U_{i'}\times_U V)\ar[rr]|{\rho_{2,i,i'}}&&\bcP((U_i\times_U V)\times_V (U_{i'}\times_U V))\\
\bcP(U)\ar[r]_{\eta_{f^{\ast}\bcU}}\ar[rru]|{\bcP(p_{2,U_i,V})}&\displaystyle\prod_{k\in I}\bcP(U_k\times_U V)\ar[rr]_{\rho_2}\ar[ur]|{\pi_{i'}} &&
\displaystyle\prod_{k,k'\in I}\bcP((U_k\times_U V)\times_V (U_{k'}\times_U V))\ar[ur]|{\pi_{i,i'}}&
} 
}
\end{equation}
Such morphisms exists by and universal property of product. That, definitions of $p_{1,U_k,V}\times_f p_{1,U_{k'},V}$ \ref{PtimesfP}, $\rho$, $\rho_1$, and $\rho_2$, $f^{\bcU}$ guarantee the commutativity of the front face. Then, straight forward calculations shows the commutativity of the back square. That implies the commutativity of the right square in \ref{Co}, which in turn implies the existence of the unique $\bcP_f(\bcU)$ that makes middle square commutate.\\
Hence, $$\ker_{\bcP,f^{\ast}\bcU}\circ \bcP_f(\bcU)\circ \eta_{\bcU}=
\displaystyle\prod_{k\in I}\bcP(p_{1,Uk,V})\circ \ker_{\bcP,\bcU}\circ \eta_{\bcU}
=\ker_{\bcP,f^{\ast}\bcU}\circ \eta_{f^{\ast}\bcU}\circ \bcP(f)$$
Since $\ker_{\bcP,f^{\ast}\bcU}$ is a monomorphism, then
$$\bcP_f(\bcU)\circ \eta_{\bcU}=\eta_{f^{\ast}\bcU}\circ \bcP(f)$$
\end{proof}
\begin{lemma}\label{PulledbackRef}
$\bcP_f(\bcU')\circ \bcP_U(\phi_{\epsilon})=\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))\circ \bcP_f(\bcU)$, i.e. the following diagram commute:
$$
\xymatrix{\bcP_U(\bcU)\ar[dd]_{\bcP_f(\bcU)}\ar[rr]^{\bcP_U(\phi_{\epsilon})}&&\bcP_U(\bcU')\ar[dd]^{\bcP_f(\bcU')}\\
\\
\bcP_V(f^{\ast}\bcU)\ar[rr]_{\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))}&&\bcP_V(f^{\ast}\bcU')
}
$$
\end{lemma}
\begin{proof}Consider the diagram:
$$
{\tiny \xymatrix{
\bcP_U(\bcU)\ar[ddddd]_{\bcP_f(\bcU)}\ar[rd]|{\ker_{\bcP,\bcU}}\ar[rrrrr]^{\bcP_U(\phi_{\epsilon})}&&&&&\bcP_U(\bcU')\ar[ddddd]^{\bcP_f(\bcU')}\ar[ld]|{\ker_{\bcP,\bcU'}}\\
&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[rd]|{\pi_{\epsilon(i')}}\ar[rrr]^{\displaystyle\prod_{l \in I'} \bcP(\phi_{l})}\ar[ddd]_{\displaystyle\prod_{k \in I} \bcP(p_1)} &&& \displaystyle\prod_{l\in I'}\bcP(U'_l)\ar[ld]|{\pi_{i'}} \ar[ddd]^{\displaystyle\prod_{l \in I'} \bcP(p_1)}  &\\
&&\bcP(U_{\epsilon(i'})\ar[r]^{\bcP(\phi_{i'})}\ar[d]_{\bcP(p_1)}&\bcP(U'_{i'})\ar[d]^{\bcP(p_1)}&&\\
&&\bcP(U_{\epsilon(i')}\times_U V)\ar[r]_{\bcP(f^{\ast}\phi_{i'})} &\bcP(U_{i'}\times_U V)&&\\
&\displaystyle\prod_{k\in I}\bcP(U_k\times_U V)\ar[ru]|{\pi_{\epsilon(i')}}\ar[rrr]_{\displaystyle\prod_{l \in I'} \bcP(f^{\ast}\phi_{l})} &&&\displaystyle\prod_{l\in I'}\bcP(U_l\times_U V)\ar[lu]|{\pi_{i'}} &\\
\bcP_V(f^{\ast}\bcU)\ar[rrrrr]_{\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))}\ar[ru]|{\ker_{\bcP,f^{\ast}\bcU}}&&&&&\bcP_V(f^{\ast}\bcU')\ar[lu]|{\ker_{\bcP,f^{\ast}\bcU'}}
}}
$$
From \ref{fastphi}, we find that the central square is commutative, $\forall i' \in I'$. Then the definition of the four product morphisms implies that the four inner diagram around it are also commutative, $\forall i' \in I'$. Also, the definition of the external morphisms implies that the outer diagrams are commutative as well. Hence, $\forall i' \in I'$:
$$\pi_{i'}\circ\ker_{\bcP,f^{\ast}\bcU'}\circ \bcP_f(\bcU')\circ \bcP_U(\phi_{\epsilon})=
\pi_{i'}\circ\ker_{\bcP,f^{\ast}\bcU'}\circ\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))\circ \bcP_f(\bcU)$$
Then using the universal property of $\displaystyle\prod_{l\in I'}\bcP(U_l\times_U V)$, we find:
$$\ker_{\bcP,f^{\ast}\bcU'}\circ \bcP_f(\bcU')\circ \bcP_U(\phi_{\epsilon})=
\ker_{\bcP,f^{\ast}\bcU'}\circ\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))\circ \bcP_f(\bcU)$$
Since $\ker_{\bcP,f^{\ast}\bcU'}$ is a monomorphism, then:
$\bcP_f(\bcU')\circ \bcP_U(\phi_{\epsilon})=\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))\circ \bcP_f(\bcU)$
\end{proof}
\begin{conclusion}\label{PulledbackRefRes}
$\bcP_f(\bcU')\circ \bcP_U(\phi_{\epsilon})=\bcP_V((\phi'_{\epsilon'}))\circ \bcP_f(\bcU)$, for any refinement morphism $\phi'_{\epsilon'}:f^{\ast}\bcU'\rightarrow f^{\ast}\bcU$ i.e. the following diagram commute:
$$
\xymatrix{\bcP_U(\bcU)\ar[dd]_{\bcP_f(\bcU)}\ar[rr]^{\bcP_U(\phi_{\epsilon})}&&\bcP_U(\bcU')\ar[dd]^{\bcP_f(\bcU')}\\
\\
\bcP_V(f^{\ast}\bcU)\ar[rr]_{\bcP_V(\phi'_{\epsilon'})}&&\bcP_V(f^{\ast}\bcU')
}
$$
\end{conclusion}
\begin{proof}
A straightforward application of \ref{PulledbackRef} and \ref{CovPro}.
\end{proof}
\begin{definition}
Let $\eta_U:\bcP(U)\rightarrow \displaystyle\Colim_{\Cov^{op}(U)}\bcP_U$ be defined by $\eta_U=i_{\bcU}\circ \eta_{\bcU}$ for some $\bcU\in \Cov(U)$, where $i_{\bcU}$ is a colimit canonical injection.
\end{definition}
\begin{lemma}\label{P+} The above defined $\eta_U$ is independent of the choice of $\bcU$.\\
Furthermore, there exist a \tcb{unique?} canonical morphism $\displaystyle\Colim_{\Cov^{op}(\bcP_U)}\rightarrow \displaystyle\Colim_{\Cov^{op}(V)}\bcP_V$ that makes the following diagram commute:
$$
\xymatrix{
\bcP(U)\ar[d]_{\bcP(f)}\ar[rr]^{\eta_U}&&\Colim_{\Cov^{op}(U)}\bcP_U\ar@{-->}[d]^{c_f}\\
\bcP(V)\ar[rr]^{\eta_V}&&\Colim_{\Cov^{op}(V)}\bcP_V\\
}
$$
\end{lemma}
\begin{proof}
$\forall \phi_{\epsilon}:\bcU'\rightarrow \bcU$ in $\Cov(U)$, from \ref{kPPhik}, and the definition of colimit canonical injections we find that:
$$\eta_U=i_{\bcU'}\circ \eta_{\bcU'}=i_{\bcU'}\circ \bcP_U(\phi_{\epsilon})\circ \eta_{\bcU}=i_{\bcU}\circ \eta_{\bcU}$$
Hence, $\eta_U$ is independent of the choice of $\bcU$.\\\\
$\forall \phi_{\epsilon}:\bcU'\rightarrow \bcU$ in $\Cov(U)$, consider the following 3D-diagram:
$${\small
\xymatrix{
\bcP(U)\ar[rr]|{\eta_{\bcU}}\ar[dd]|{\bcP(f)}\ar[rrrrddd]^{\eta_{\bcU'}}&&\bcP_U(\bcU)\ar[rrddd]|{\bcP_U(\phi_{\epsilon})}\ar[rrr]|{i_{\bcU}}\ar@{..>}[dd]|{\bcP_f(\bcU)}&&&\Colim_{\Cov^{op}(U)}\bcP_U\ar@{-->}[dd]|{c_f}\\
\\
\bcP(V)\ar@{..>}[rr]|{\eta_{f^{\ast}\bcU}}\ar[rrrrddd]|{\eta_{f^{\ast}\bcU'}}&&\bcP_V(f^{\ast}\bcU)\ar@{..>}[rrddd]|{\bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))}\ar@{..>}[rrr]|{i_{f^{\ast}\bcU}}&&&\Colim_{\Cov^{op}(V)}\bcP_V\\
&&&&\bcP_U(\bcU')\ar[dd]|{\bcP_f(\bcU')}\ar[ruuu]|{i_{\bcU'}}\\
\\
&&&&\bcP_V(f^{\ast}\bcU')\ar[ruuu]|{i_{f^{\ast}\bcU'}}
}}
$$
From \ref{PulledbackRef}, and definition of consider morphisms, we find that the left side 3D-partial-diagram commutes. Hence, based on the definition of the colimit canonical injections, we find that:
$$
i_{f^{\ast}\bcU}\circ \bcP_f(\bcU)= i_{f^{\ast}\bcU'}\circ \bcP_V(\hat{f}^{\ast}(\phi_{\epsilon}))\circ \bcP_f(\bcU)=
\left( i_{f^{\ast}\bcU'}\circ \bcP_f(\bcU'	)\right)\circ \bcP_U(\phi_{\epsilon})
$$
Then, using the universal property of $\Colim_{\Cov^{op}(U)}\bcP_U$, we find that $\exists! c_f:\Colim_{\Cov^{op}(U)}\bcP_U\rightarrow \Colim_{\Cov^{op}(V)}\bcP_V$ such that $f_c\circ i_{\bcU}=i_{f^{\ast}\bcU}\circ \bcP_f(\bcU),\forall \bcU \in \Cov(U)$. I.e. $c_f$ makes the hole diagram commutative.

\tcg{show uniqueness in sense of the statement of the lemma}
\end{proof}
\begin{definition}[\tcr{Associated Pre-sheaf}]
We define $\bcP^+(U)=\displaystyle\Colim_{\Cov^{op}(U)}\bcP_U$, and $\bcP^+(f)=c_f$, where $c_f$ is defined in the above lemma.
\end{definition}
\begin{proposition}
$\bcP^+$ is an abelain pre-sheaf.
\end{proposition}
\begin{proof}
The definition of $\bcP^+(f)$ using the universal property guarantee that $\bcP^+:\bcC^{op}\rightarrow \bcA$ is a functor, hence a $\bcA$-valued pre-sheaf on $\bcC$, i.e. an abelain pre-sheaf.
\end{proof}
\begin{corollary}
The collection $\eta_{\bcP}:=\{\eta_{\bcP,U}|U\in ob{\bcU}\}$ defines a morphism of pre-sheaves $\eta_{\bcP}:\bcP\rightarrow \bcP^+$
\end{corollary}
\begin{proof}
\ref{P+} implies that $\eta:\bcP\stackrel{\cdot}{\rightarrow}\bcP^{+}$ is a natural transformation. Hence, it is a morphism of pre-sheaves.
\end{proof}
\begin{corollary}\label{NT-eta}
The collection $\eta:=\{\eta_{\bcP}|\bcP\in \PreC\}$ defines a natural transformation $\eta:Id\stackrel{\cdot}{\rightarrow} -^+$
\end{corollary}
\begin{proof}
\tcb{type the proof. (also, it commutes by the definition of $\varphi^+$)}
\end{proof}

\begin{lemma}
$\varphi:\bcP\rightarrow \bcQ$ induce a canonical morphism of pre-sheaves $\varphi^+:\bcP^+\rightarrow \bcQ^+$ that makes $-^+:\PreC\rightarrow \PreC$ a functor.
\end{lemma}
\begin{proof}
$\forall U \in \bcC$, $\varphi_U:\bcP\rightarrow \bcQ_U$ is a natural transformation, lemma \ref{NT_U}. Hence, the following diagram commute $\forall (\epsilon,\phi):\bcU'\rightarrow \bcU$ in $\Cov(U)$:
$$
\xymatrix{
\bcP_U(\bcU)\ar[r]^{\bcP_U((\epsilon,\phi))}\ar[d]_{\varphi_U(\bcU)}&\bcP_U(\bcU')\ar[d]^{\varphi_U(\bcU')}\\
\bcQ_U(\bcU)\ar[r]_{\bcQ_U((\epsilon,\phi))}&\bcQ_U(\bcU')
}
$$
Then, $\forall (\epsilon,\phi):\bcU'\rightarrow \bcU$ in $\Cov(U)$, there is a morphism $i'_{\bcU}:=i_{\bcQ,\bcU}\circ \varphi_U(\bcU)$ such that:\\
$i'_{\bcU'}\circ \bcP_U((\epsilon,\phi))=\left(i_{\bcQ,\bcU'}\circ \varphi_U(\bcU')\right)\circ \bcP_U((\epsilon,\phi))=i_{\bcQ,\bcU'}\circ \left(\bcQ_U((\epsilon,\phi))  \circ \varphi_U(\bcU)\right) =i_{\bcQ,\bcU}\circ \circ \varphi_U(\bcU)=i'_{\bcU}$\\
Hence, by the universal property of the colimit $\bcP^+(U)$, $\exists! \varphi^+(U):\bcP^+(U)\rightarrow\bcQ^+(U)$ that makes the following diagram commute $\forall (\epsilon,\phi):\bcU'\rightarrow \bcU$ in $\Cov(U)$:
$${\small
\xymatrix{
\bcP_U(\bcU)\ar[drrr]|{i_{\bcP,\bcU}}\ar[rr]^{\bcP_U((\epsilon,\phi))}\ar[dd]_{\varphi_U(\bcU)}&&\bcP_U(\bcU')\ar@{..>}[dd]^{\varphi_U(\bcU')}\ar[dr]|{i_{\bcP,\bcU'}}\\
&&&\bcP^+(U)\ar@{-->}[dd]^{\varphi^+(U)}\\
\bcQ_U(\bcU)\ar[drrr]|{i_{\bcQ,\bcU}}\ar@{..>}[rr]^{\bcQ_U((\epsilon,\phi))}&&\bcQ_U(\bcU')\ar\ar@{..>}[dr]|{i_{\bcQ,\bcU'}}\\
&&&\bcQ^+(U)
}}
$$
We need to show that $\varphi^+:=\{\varphi^+(U)|U\in \bcC\}$ is a morphism of pre-sheaves, i.e. a natural transformation. $\forall f:V\rightarrow U$ in $\bcC$

\tcg{!!!!!!!!!!!!!!}

Hence, $\varphi^+$ is a morphism of pre-sheaves.\\
Since, $\bcP^+$ is a pre-sheaf, and $-^+$ is defined on arrow using universal property. Then, $-^+:\PreC\rightarrow\PreC$ is a functor.
\end{proof}

\begin{lemma}
$\eta_-:Id\stackrel{\cdot}{\rightarrow} -^+:\PreC\rightarrow \PreC$ is a natural transformation.
\end{lemma}
\begin{proof}
!!!!
\end{proof}


\begin{fact}[Colimit in $\Sets$ over $\Cov(U)$]
$\Colim_{\Cov(U)}\bcP_U=\displaystyle\bigsqcup_{\bcU\in \Cov(U)}\bcP_U(\bcU) \diagup \thicksim$.
Where $\thicksim$ is an equivalence relation, defined by $x\thicksim y \Longleftrightarrow x\in \bcP(\bcU_x),y\in \bcP(\bcU_y)$ such that there is a common refinement $\bcU$ with refinement morphisms $\phi_{x,\epsilon_x}:\bcU\rightarrow \bcU_x$, $\phi_{y,\epsilon_y}:\bcU\rightarrow \bcU_y$ such that $\bcP_U(\phi_{y,\epsilon_y})(y)=\bcP_U(\phi_{x,\epsilon_x})(x)$.
\end{fact}
\begin{proof}
\tcg{type the proof}.
\end{proof}

\begin{lemma}\label{RefMono}
If $\rho_{\bcU'}$ is a monomorphism, then $\rho_{\bcU}$ is a monomorphism.
\end{lemma}
\begin{proof}
Consider the commutative diagram, $\forall i'\in I'$:
$$
\xymatrix{\bcP(U)\ar[rr]|{\rho_{\bcU}}\ar[rrd]_{\bcP(f_{\epsilon(i')})}&&\displaystyle\prod_{k\in I} \bcP(U_k)\ar[d]|{\pi_{\epsilon(i')}}\ar[rrrr]|{\small \displaystyle\prod_{l\in I'}\bcP(\phi_l)}&&&&\displaystyle\prod_{l\in I'}\bcP(U'_l)\ar[d]^{\pi_{i'}}\\
&&\bcP(U_{\epsilon(i')})\ar[rrrr]_{\bcP(\phi_{i'})}&&&&\bcP(U'_{i'})
}
$$
Since $f'_{i'}=f_{\epsilon(i')}\circ \phi_{i'}, \forall i'\in I'$, and based on the definition of $\rho$, we find that
$$\rho_{\bcU'}={\displaystyle\prod_{l\in I'}\bcP(\phi_l)}\circ \rho_{\bcU}$$
Hence, if $\rho_{\bcU'}$ is a monomorphism, then $\rho_{\bcU}$ is a monomorphism.
\end{proof}
\begin{remark}
The above lemma is useful in showing that some pre-sheaf is separated. That, we do not need to verify the separability criterion for every covering, but rather, or an appropriate choice of their refinements.
\end{remark}
\tcr{how to draw element diagram inside sets diagram?}



\begin{proposition}\label{SepPreSh}
Let $\bcP \in \PreC$, if $\bcA$ is the abelian category $\Sets$ or $\Ab$, $\bcP^+$ is a separated pre-sheaf.
\end{proposition}
\begin{proof}
Let $U\in \bcC,\bcU=\{f_i:U_i\rightarrow U|i\in I\}\in \Cov(U)$. We need to show that $\rho_{\bcU}$ is a monomorphism. Since $\bcA$ is either the abelian category $\Ab$, or $\Sets$, that is equivalent of showing that $\rho_{\bcU}$ is an injection.\\

Let $x,y\in \bcP^+(U):\rho_{\bcU}(x)=\rho_{\bcU}(y)$,\\
We consider the following diagram, constructed as follows, $\forall j\in J, j'\in J'_j$:
$$
{\tiny \xymatrix{
&&\displaystyle\prod_{k\in I}\bcP^+(U_k)\ar[rrr]^{{\tiny \displaystyle\prod_{l\in  J}\bcP^+(\varphi_l)}}&&&\displaystyle\prod_{l\in J}\bcP^+(V_l)\ar[d]^{\pi_{j}}\\
\bcP^+(U)\ar[rru]^{\rho_{\bcU}}\ar[rrrrru]_{\rho_{\bcV}}\ar[rrrrr]_{\bcP^+(g_j)}&&&&&\bcP^+(V_j)\\
\bcP_U(\bcV)\ar[dr]_{\bcP_U(\psi_{\epsilon})}\ar[u]^{i_{\bcV}}\ar@{..>}[rrrrr]_{\bcP_{g_j}(\bcV)}&&&&&\bcP_{V_j}
(g_j^{\ast}\bcV)\ar@{..>}[u]|{i_{g_j^{\ast}\bcV}}\ar@{..>}[dl]|{\bcP_{V_j}(g_j^{\ast}\psi_{\epsilon})}\ar@{..>}[dr]&&\\ 
&\bcP_U(\bcV')\ar@{_(->}[d]_{\ker_{\bcP,\bcV'}}\ar@/_/[luu]|{i_{\bcV'}}\ar[rrr]_{\bcP_{g_j}(\bcV')}&&&\bcP_{V_j}
(g_j^{\ast}\bcV')\ar@{_(->}[d]|{\ker_{\bcP,g_j^{\ast}\bcV'}}\ar[rr]_{{\tiny \bcP_{V_j}(\phi_{j,id})}} \ar@/^/[ruu] &&\bcP_{V_j}(\bcV'_j)\ar@/_/[luu]|{i_{\bcV'_j}}\ar@{_(->}[d]|{\ker_{\bcP,\bcV'_j}}\\
&\displaystyle\prod_{(l,l')\in J'}\bcP(V'_{ll'})\ar[rrr]_{{\tiny \displaystyle\prod_{(l,l')\in J'}\bcP(p_{1,V'_{ll'},V_j})}}\ar@{=}[d]&&&\displaystyle\prod_{(l,l')\in J'}\bcP(V'_{ll'}\times_U V_j)\ar[rr]_{\bcP(\phi_{jj'})\circ \pi_{jj'}}&&\bcP(V'_{jj'})\ar@{=}[d]\\
&\displaystyle\prod_{(l,l')\in J'}\bcP(V'_{ll'})\ar[rrrrr]_{\pi_{jj'}}&&&&&\bcP(V'_{jj'})
}}
$$
Based on the definition of $\bcP^+(U)$, there exist $\bcU_x,\bcU_y \in \Cov(U)$ such that $x=[x_{\bcU_x}],y=[y_{\bcU_y}]$, for some $x_{\bcU_x}\in \bcP_U(\bcU_x),y_{\bcU_y}\in \bcP_U(\bcU_x)$.\\
Let $\bcV=\{g_j:V_j\rightarrow U|j\in J\}$ be a common refinement of $\bcU,\bcU_x$ and $\bcU_y$ with the refinement morphisms $\varphi_{x,\varepsilon_x}:\bcV\rightarrow \bcU_x,\varphi_{y,\varepsilon_y}:\bcV\rightarrow \bcU_y$,  $\varphi_{\varepsilon}:\bcV\rightarrow \bcU$.\\
Then, $\rho_{\bcV}(x)=\displaystyle\prod_{l\in J}\bcP^+(\varphi_l)(\rho_{\bcU}(x))=\displaystyle\prod_{l\in J}\bcP^+(\varphi_l)(\rho_{\bcU}(y))=\rho_{\bcV}(y)$. Which implies the commutativity of the upper partial diagram. Where, $\displaystyle\prod_{l\in J}\bcP^+(\varphi_l)$ is defined in \ref{RefProd}. Hence, $\bcP^+(g_j)(x)=\bcP^+(g_j)(y), \forall j\in J$. \\
Let $x_{\bcV}:=\bcP_U(\varphi_{x,\varepsilon_x})(x_{\bcU_x}),y_{\bcV}:=\bcP_U(\varphi_{y,\varepsilon_y})(y_{\bcU_y})\in \bcP_U(\bcV)$, i.e. $x=[x_{\bcV}]$ and $y=[y_{\bcV}]$.\\
Then, $\forall j\in J, [\bcP_{g_j}(\bcV)(x_{\bcV})]=[\bcP_{g_j}(\bcV)(y_{\bcV})]$. Hence, there exist 
$\bcV'_j=\{g'_{jj'}:V'_{jj'}\rightarrow V_j|j'\in J'_j\}\in \Cov(V_j)$, and there are refinement morphisms $g_j^{\ast}\psi_{\epsilon}\circ \phi_{j,id}:\bcV'_j\rightarrow g_j^{\ast}\bcV$ ,(\ref{RefTh}), such that:\\
$\bcP_{V_j}(g_j^{\ast}\psi_{\epsilon}\circ \phi_{j,id})(\bcP_{g_j}(\bcV)(x_{\bcV}))=\bcP_{V_j}(g_j^{\ast}\psi_{\epsilon}\circ \phi_{j,id})(\bcP_{g_j}(\bcV)(y_{\bcV}))$.\\
Let $J'$, and $\bcV'$ as in \ref{RefTh}. $\bcV'$ is a refinement of $\bcU'$ with the refinement morphism $\psi_{\epsilon}:\bcV'\rightarrow \bcV$,(\ref{RefTh}).\\
Then, the partial 3D-diagram commutes,\ref{PulledbackRef}, and
\begin{equation}\label{Rep}
\bcP_{V_j}(\phi_{j,id})\circ  \bcP_{g_j}(\bcV')(x_{\bcV'})=\bcP_{V_j}(\phi_{j,id})\circ  \bcP_{g_j}(\bcV')(y_{\bcV'}),\forall j\in J
\end{equation}
Where, $x_{\bcV'}=\bcP_U(\psi_{\epsilon})(x_{\bcV})$ and $y_{\bcV'}=\bcP_U(\psi_{\epsilon})(y_{\bcV})$, i.e. $x=[x_{\bcV'}]$ and $y=[y_{\bcV'}]$.\\
The commutativity of the partial diagrams below is a straightforward result of the definitions of $\bcP_{g_j}(\bcV')$, and $\bcP_{V_j}(\phi_{j,id})$.
The commutativity of the lower diagram is due to the definition of $\displaystyle\prod_{(l,l')\in J'}\bcP(p_{1,V'_{ll'},V_j})$ in \ref{CoDetailes}, and $\phi_{jj'}$ in \ref{RefTh} that, $\forall (j,j') \in J'$:\\
$\bcP(\phi_{jj'})\circ\pi_{jj'}\circ \displaystyle\prod_{(l,l')\in J'}\bcP(p_{1,V'_{ll'},V_j})=
\bcP(\phi_{jj'})\circ \bcP(p_{1,V'_{jj'},V_j})\circ \pi_{jj'}=\\
\bcP(p_{1,V'_{jj'},V_j}\circ \phi_{jj'})\circ \pi_{jj'}=
\bcP(id_{V'_{jj'}})\circ \pi_{jj'}= \pi_{jj'}$\\
Using \ref{Rep} and the commutativity of the above diagram, we find that
$$\left(\pi_{jj'}\circ \ker_{\bcP,\bcV'}\right)(x_{\bcV'})=\left(\pi_{jj'}\circ \ker_{\bcP,\bcV'}\right)(y_{\bcV'}),\forall (jj')\in J'$$
Hence, $\ker_{\bcP,\bcV'}(x_{\bcV'})= \ker_{\bcP,\bcV'}(y_{\bcV'})$ (Using the universal property of $\displaystyle\prod_{(l,l')\in J'}\bcP(V'_{ll'})$). Since, $\ker_{\bcP,\bcV'}$ is a monomorphis, then $x_{\bcV'}=y_{\bcV'}$.  Hence, $x=[x_{\bcV'}]=[y_{\bcV'}]=y$. Therefore, $\rho_{\bcU}$ is a monomorphism, and $\bcP^+$ is separated.
\end{proof}
\begin{remark}
We notice that having $\bcA$ either the category $\Sets$ or $\Ab$, enable us to prove injectivity using elements. Having $\Cov(U)$ being a filtering category provides fine enough refinements to tern the problem to proving injectivity on the level of that covering instead of proving it for the colimit. Which is correct in tern, due to the universal property of $\ker,\times_U$ and $\displaystyle\prod$.\\
Having $\ker$ being a monomorphism has been used explicitly, wherears its universal property has been used implicitly to construct the diagram.
\end{remark}
\begin{counterexample}[A pre-sheaf with $\rho$ not a monomorphism]
\tcg{type the example with $\rho$ not a monomorphism. should be a presheaf not sheaf}!!
\end{counterexample}
\begin{lemma}\label{SepLem}
Let $\bcP \in \PreC$, for any  abelian category $\bcA$, and $\bcP$ is separated, then for every refinement morphism $\bcU'=\{g_j:U'_{i'}\rightarrow U|i'\in I'\}\stackrel{\phi_{\epsilon}}{\longrightarrow}\bcU=\{f_i:U_i\rightarrow U|i\in I\}$, $\bcP_U(\phi_{\epsilon})$ is a monomorphism.
\end{lemma}
\begin{proof}
From the definition of $|cov(U)$, and \ref{CommonRef}, we have the commutative diagram in $\Cov(U)$:
$$
\xymatrix{\bcU\times\bcU'\ar[r]^{Pr_1}\ar[d]_{Pr_2}&\bcU\\
\bcU'\ar[ru]_{\phi_{\epsilon}}
}
$$
That induce the following commutative diagram in $A$:
$${\small
\xymatrix{\bcP_U(\bcU\times\bcU')&&\bcP_U(\bcU)\ar[ll]_{\bcP_U(Pr_1)}\ar[ddll]^{\bcP_U(\phi_{\epsilon})}\\\\
\bcP_U(\bcU')\ar[uu]^{\bcP_U(Pr_2)}
}}
$$
Therefore, if $\bcP_U(Pr_1)$ is a monomorphism, then $\bcP_U(\phi_{\epsilon})$ is a monomorphism.\\
Let $\xymatrix{A\ar@<+2pt>[rr]^{g}\ar@<-2pt>[rr]_{g'}&&\bcP_U(\bcU)}$ such that $\bcP_U(Pr_1)\circ g=\bcP_U(Pr_1)\circ g'$. Then, consider the commutative diagram, $\forall i\in I$:
$$
{\tiny \xymatrix{
A\ar@<+2pt>[rr]^{g}\ar@<-2pt>[rr]_{g'}&&\bcP(\bcU)\ar[rrrrr]^{\bcP_U(Pr_1)}\ar@{_(->}[d]_{\ker{\bcP,\bcU}}&&&&&\bcP_U(\bcU\times\bcU')\ar@{_(->}[d]^{\ker{\bcP,\bcU\times\bcU'}}\\
&&\displaystyle\prod_{k\in I}\bcP(U_k)\ar[d]_{\pi_i}\ar[rrrrr]^{\displaystyle\prod_{(k,k')\in I\times I'}\bcP(p_{1,k,k'})}&&&&&\displaystyle\prod_{(k,k')\in I\times I'}\bcP(U_k\times_U U_{k'})\ar[d]^{\displaystyle\prod_{k'\in I'}\pi_{ik'}}\\
&&\bcP(U_i)\ar@{^(->}[rrrrr]^{\rho_{f_i^{\ast}\bcU'}=\displaystyle\prod_{k'\in I'}\bcP(p_{1,i,k'})}&&&&&\displaystyle\prod_{k'\in I'}\bcP(U_i\times_U U_{k'})
}}
$$
The commutativity of the above diagram is due to the definition of $\bcP_U(Pr_2)$ (\ref{H0(-,-)}). Having $\bcP$ seperated implies that $\rho_{f_i^{\ast}\bcU'}$ is a monomorphism. Then, the above relation and the commutativity of the diagram implies that:
$$
\rho_{f_i^{\ast}\bcU'}\circ \pi_i\circ \ker_{\bcP,\bcU}\circ g=\rho_{f_i^{\ast}\bcU'}\circ \pi_i\circ \ker_{\bcP,\bcU}\circ g'\  ,\forall i\in I
$$
Since, $\rho_{f_i^{\ast}\bcU'}$ is a monomorphism, we have:
$$
\pi_i\circ \ker_{\bcP,\bcU}\circ g= \pi_i\circ \ker_{\bcP,\bcU}\circ g'\  ,\forall i\in I
$$
Then, based on the universal property of $\displaystyle\prod_{k\in I}\bcP(U_k)$, we have:
$$
\ker_{\bcP,\bcU}\circ g=\ker_{\bcP,\bcU}\circ g'\  ,\forall i\in I
$$
$\ker_{\bcP,\bcU}$ is a monomorphis. Then, $g=g'$, and $\bcP_U(Pr_1)$ is a monomorphism. Hence, $\bcP_U(\phi_{\epsilon})$ is a monomorphism.
\end{proof}
\begin{conclusion}
Let $\bcP \in \PreC$, for any  abelian category $\bcA$, and $\bcP$ is separated, then:
\begin{itemize}
\item The canonical morphism $\eta_{\bcU}:\bcP(U)\rightarrow \bcP_U(\bcU)$ is a monomorphism.
\item If $\bcA$ is the category $\Sets$ or $\Ab$, then the canonical injection $i_{\bcU}:\bcP_U(\bcU)\rightarrow \bcP^+(U)$ is a monomorphism.
\item If $\bcA$ is the category $\Sets$ or $\Ab$, then $\eta:\bcP\rightarrow\bcP^+$ is a monomorphism.\tcb{prove it general, or counter example}.
\end{itemize}
\end{conclusion}
\begin{proof}:\\
\begin{itemize}
\item There is $\bcU_{\{\emptyset\}}:\bcU\rightarrow\{id_U\}$ a refinement morphism, \ref{RefTh}, Hence $\bcP_U(\bcU_{\{\emptyset\}})$ is a monomorphism. But, straight forward calculations shows that $\bcP_U(\{id_U\})=\bcP(U)$, and $\eta_{\bcU}=\bcP_U(\bcU_{\{\emptyset\}})$.
\item Let $x,y \in \bcP_U(\bcU)$ such that $i_{\bcU}(x)=[x]=[y]=i_{\bcU}(y)$. Then, there exist a refinement morphism $\phi_{\epsilon}:\bcU'\rightarrow \bcU$ such that $\bcP_U(\phi_{\epsilon})(x)=\phi_{\epsilon}(y)\in \bcP(\bcU')$. $\bcP_U(\phi_{\epsilon})$ is a monomorphism, then $x=y$ and $i_{\bcU}$ is a monomorphism.
\tcb{Try to prove it in general}
\item $\eta$ is a natural transformation, so it is a monomorphism iff $\eta_U$ is a monomorphism $\forall U\in \bcC$.\\
Let $U\in \bcC$, then $\eta_U=i_{\bcU}\circ \eta_{\bcU}$ is a monomorphis.
\item Another proof of last point:\\
Let $U\in \bcC, x,y \in \bcP(U)$ such that $\eta_U(x)=\eta_U(y)\in \bcP^+(U)$, then similar argument to \ref{SepPreSh} implies that $\exists \bcU\in \Cov(U)$ such that $\eta_{\bcU}(x)=\eta_{\bcU}(y)\in \bcP_U(\bcU)$.\\
Consider the following commutative diagram:
$$
\xymatrix{	
&&\bcP^+(U)\\
\bcP(U)\ar[rru]^{\eta_U}\ar[rr]|{\eta_{\bcU}}\ar[rrd]_{\rho_{\bcU}}&&\bcP_U(\bcU)\ar[u]_{i_{\bcU}}\ar[d]^{\ker_{\bcP,\bcU}}\\
&&\displaystyle\prod_{k\in I}\bcP(U_k)
}
$$
Since $\bcP$ is separated, then $\rho_{\bcU}$ is a monomorphism. Hence, $\eta_{\bcU}$ is a monomorphism. Therefore, $x=y$, and $\eta_U$ is a monomophism. Therefore, $\eta$ is a monomorphism.
\tcb{check(} \tcr{is the colimit of monomorphis is a monomorphism?)}
\end{itemize}
\end{proof}
\begin{proposition}
Let $\bcP \in \PreC$, if $\bcA$ is the either the abelian category $\Ab$, or $\Sets$ and $\bcP$ is separated, $\bcP^+$ is a sheaf.
\end{proposition}
\begin{proof}
Let $U\in \bcC, \bcU\in \Cov(U)$, we need to show that $\Ker(\rho_1,\rho_2)=\Imm(\rho)$. From, \ref{p1p=p2p}, we have that $\Imm(\rho)\subseteq \Ker(\rho_1,\rho_2)$, then we need just to prove the opposite inclusion:\\
Let $x\in \Ker(\rho_1,\rho_2)$, i.e. $x\in \displaystyle\prod_{k\in I}\bcP^+(U_k)$ such that $\rho_1(x)=\rho_2(x)$.\\
$\forall i \in I$, Let $x_i:=\pi_i(x)\in \bcP^+(U_i)$. Hence, there exists $\bcV_i=\{g_{ij}:V_{ij}\rightarrow U|j\in J_i\}\in \Cov(U_i)$ and $x_{\bcV_i}\in \bcP_{U_i}(\bcV_i):\ x=[x_{\bcV_i}]=i_{\bcV_i}(x_{\bcV_i})$. Let $\bcV:=\bcU\{\bcV_i|i\in I\}$, then \ref{RefTh}, implies that $\bcV\in \Cov(U)$.\\
Consider the following two diagram, constructed as follows, $\forall i,i'\in I,j\in J_i,j'\in J_{i'}$:
The first rows of cells commute due to the definition of $\rho,\rho_1$ and $\rho_2$. The second and third rows of cells commute due to \ref{RefTh2}, \ref{RefDiffObj}, \ref{Phiii'} and \eqref{H_U^0_1}. Notice that:\\
$\pi_{ij,i'j'}\circ {\displaystyle\prod_{l\in J_i,l'\in J_{i'}}\bcP(\phi_{1,i,i',l,l'})}\circ {\displaystyle\prod_{l\in J_i}\bcP(p_{1,V_{il},(U_i\times_U U'_{i'})})} \circ {\displaystyle\prod_{l\in J_i}\pi_{il}}=\\
\bcP(\phi_{1,i,i',j,j'})\circ \pi_{j}  \circ {\displaystyle\prod_{l\in J_i}\bcP(p_{1,V_{il},(U_i\times_U U'_{i'})})} \circ {\displaystyle\prod_{l\in J_i}\pi_{il}}=\\
\bcP(\phi_{1,i,i',j,j'})\circ {\bcP(p_{1,V_{ij},(U_i\times_U U'_{i'})})} \circ \pi_{j}  \circ  {\displaystyle\prod_{l\in J_i}\pi_{il}}=
\bcP(\phi_{1,i,i',j,j'})\circ {\bcP(p_{1,V_{ij},(U_i\times_U U'_{i'})})} \circ \pi_{ij}	=\\
\bcP( p_{1,V_{ij},(U_i\times_U U'_{i'})} \circ \phi_{1,i,i',j,j'}) \circ \pi_{ij}=\bcP(p_{1,V_{ij},V_{i'j'}})\circ \pi_{ij}=\pi_{ij,i'j'}\circ \rho_1$\\
The last two equality is due to $\ref{Phiii'}$ and the definition of $\rho_1$. Similar argument shows that:\\
$
\pi_{ij,i'j'}\circ {\displaystyle\prod_{l\in J_i,l'\in J_{i'}}\bcP(\phi_{2,i,i',l,l'})}\circ {\displaystyle\prod_{l'\in J_{i'}}\bcP(p_{1,V_{i'l'},(U_i\times_U U'_{i'})})} \circ {\displaystyle\prod_{l'\in J_{i'}}\pi_{i'l'}}
=\pi_{ij,i'j'}\circ \rho_2$\\
Then, the fourth rows of cells commute. Hence, the two diagram commute, $\forall i,i'\in I,j\in J_i,j'\in J_{i'}$:\\

${\tiny
\xymatrix{
&&\displaystyle\prod_{k\in I}\bcP^+(U_k)\ar[rrrr]^{\rho_1}\ar[d]|{\pi_i}&&&&\displaystyle\prod_{k,k'\in I}\bcP^+(U_k\times_U U_{k'})\ar[d]^{\pi_{ii'}}\\
\bcP^+(U)\ar@{_(->}@/^/[rru]^{\rho}\ar[rr]^{\bcP^+(f_i)}&& \bcP^+(U_i)\ar[rrrr]^{p_{1,i,i'}}&&&&\bcP^+(U_i\times_U U_{i'})\\
\bcP_U(\bcV)\ar@{_(->}[u]^{i_{\bcV}}\ar@{^(->}[d]_{\tcr{\ker}}\ar[rr]^{\bcP_{U_i}(\phi_{i,id})\circ \bcP_{f_i}(\bcV)}&&
\bcP_{U_i}(\bcV_i)\ar@{_(->}[u]^{i_{\bcV_i}}\ar@{^(->}[d]_{\ker}\ar[rr]^{\bcP_{p_{1,i,i'}}(\bcV_i)}&&
\bcP_{U_i\times_U U_{i'}}(p_1^{\ast}\bcV_i)\ar@{_(->}[urr]|{i_{p_1^{\ast}\bcV_i}}\ar@{^(->}[d]|{\ker}\ar[rr]^{\bcP_{U_i\times_U U_{i'}}(\tcb{\phi_{1,i,i'}})}&&
\bcP_{U_i\times_U U_{i'}}(\bcV_i\times_U\bcV_{i'})\ar@{_(->}@[red][u]_{\tcr{i_{\bcV_i\times_U\bcV_{i'}}}}\ar@{^(->}[d]^{\ker}\\
\displaystyle\prod_{k\in I,l\in J_k}\bcP(V_{kl})\ar[rr]^{\displaystyle\prod_{l\in J_i}\pi_{il}}&&
\displaystyle\prod_{l\in J_i}\bcP(V_{il})\ar[rr]^{\displaystyle\prod_{l\in J_i}\bcP(p_{1,V_{il},(U_i\times_U U_{i'})})}&&
\displaystyle\prod_{l\in J_i}\bcP(V_{il}\times_{U_i}(U_i\times_U U_{i'}))\ar[rr]^{\displaystyle\prod_{l\in J_i,l'\in J_{i'}}\bcP(\phi_{1,i,i',l,l'})}&&
\displaystyle\prod_{l\in J_i,l'\in J_{i'}}\bcP(V_{il}\times_U V_{i'l'})\ar[d]^{\pi_{j,j'}}\\
\displaystyle\prod_{k\in I,l\in J_k}\bcP(V_{kl})\ar[rrrr]^{\rho_1}\ar@{=}[u]&&&&
\displaystyle\prod_{k,k'\in I,l\in J_k,l'\in J_{k'}}\bcP(V_{kl}\times_U V_{k'l'})\ar[rr]^{\pi_{ij,i'j'}}&&
\bcP(V_{ij}\times_U V_{i'j'})
}}
\\
{\tiny
\xymatrix{
&&\displaystyle\prod_{k'\in I}\bcP^+(U_{k'})\ar[rrrr]^{\rho_2}\ar[d]|{\pi_{i'}}&&&&\displaystyle\prod_{k,k'\in I}\bcP^+(U_{k'}\times_U U_{k})\ar[d]^{\pi_{i'i}}\\
\bcP^+(U)\ar@{_(->}@/^/[rru]^{\rho}\ar[rr]^{\bcP^+(f_{i'})}&& \bcP^+(U_{i'})\ar[rrrr]^{p_{2,i,i'}}&&&&\bcP^+(U_{i}\times_U U_{i'})\\
\bcP_U(\bcV)\ar@{_(->}[u]^{i_{\bcV}}\ar@{^(->}[d]_{\tcr{\ker}}\ar[rr]^{\bcP_{U_{i'}}(\phi_{i',id})\circ \bcP_{f_{i'}}(\bcV)}&&
\bcP_{U_{i'}}(\bcV_{i'})\ar@{_(->}[u]^{i_{\bcV_{i'}}}\ar@{^(->}[d]_{\ker}\ar[rr]^{\bcP_{p_{2,i,i'}}(\bcV_{i'})}&&
\bcP_{U_{i}\times_U U_{i'}}(p_2^{\ast}\bcV_{i'})\ar@{_(->}[urr]|{i_{p_2^{\ast}\bcV_{i'}}}\ar@{^(->}[d]|{\ker}\ar[rr]^{\bcP_{U_{i}\times_U U_{i'}}(\tcb{\phi_{2,i,i'}})}&&
\bcP_{U_{i}\times_U U_{i'}}(\bcV_{i}\times_U\bcV_{i'})\ar@{_(->}@[red][u]_{\tcr{i_{\bcV_{i}\times_U\bcV_{i'}}}}\ar@{^(->}[d]^{\ker}\\
\displaystyle\prod_{k'\in I,l'\in J_{k'}}\bcP(V_{k'l'})\ar[rr]^{\displaystyle\prod_{l'\in J_{i'}}\pi_{i'l'}}&&
\displaystyle\prod_{l'\in J_{i'}}\bcP(V_{i'l'})\ar[rr]^{\displaystyle\prod_{l'\in J_{i'}}\bcP(p_{1,V_{i'l'},(U_{i}\times_U U_{i'})})}&&
\displaystyle\prod_{l'\in J_{i'}}\bcP(V_{i'l'}\times_{U_{i'}}(U_{i}\times_U U_{i'}))\ar[rr]^{\displaystyle\prod_{l'\in J_{i'},l\in J_{i}}\bcP(\phi_{2,i,i',l,l'})}&&
\displaystyle\prod_{l'\in J_{i'},l\in J_{i}}\bcP(V_{il}\times_U V_{i'l'})\ar[d]^{\pi_{j,j'}}\\
\displaystyle\prod_{k'\in I,l'\in J_{k'}}\bcP(V_{k'l'})\ar[rrrr]^{\rho_2}\ar@{=}[u]&&&&
\displaystyle\prod_{k,k'\in I,l\in J_{k},l'\in J_{k'}}\bcP(V_{kl}\times_U V_{k'l'})\ar[rr]^{\pi_{i'j',ij}}&&
\bcP(V_{ij}\times_U V_{i'j'})
}}
$\\
$\rho_1(x)=\rho_2(x)\rightarrow \pi_{ii'}(\rho_1(x))=\pi_{ii'}(\rho_2(x)),\forall i,i'\in I$. Then, the commutativity of the tow diagrams implies that:\\
$i_{\bcV_{i}\times_U\bcV_{i'}}( {\bcP_{U_{i}\times_U U_{i'}}(\tcb{\phi_{1,i,i'}})} \circ \bcP_{p_{1,i,i'}}(\bcV_i) (x_{\bcV_i}) )=
i_{\bcV_{i}\times_U\bcV_{i'}}( {\bcP_{U_{i}\times_U U_{i'}}(\tcb{\phi_{2,i,i'}})} \circ \bcP_{p_{2,i,i'}}(\bcV_{i'}) (x_{\bcV_{i'}})  )
$\\
Since $\bcP$ is separated, then $i_{\bcV_{i}\times_U\bcV_{i'}}$ is a monomorphism and:\\
\begin{equation}\label{Eq-1}
{\bcP_{U_{i}\times_U U_{i'}}(\tcb{\phi_{1,i,i'}})} \circ \bcP_{p_{1,i,i'}}(\bcV_i) (x_{\bcV_i}) ={\bcP_{U_{i}\times_U U_{i'}}(\tcb{\phi_{2,i,i'}})} \circ \bcP_{p_{2,i,i'}}(\bcV_{i'}) (x_{\bcV_{i'}}) 
\end{equation}
Let $\ker_{\bcP,\bcV_i}(x_{\bcV_i})=\displaystyle\prod_{l\in J_i}x_{il}$, where $x_{ij}\in \bcP(V_{ij})\forall i\in I, j\in J_i$. Then, using the universal property of $\displaystyle\prod_{k\in I,l\in J_k}\bcP(V_{kl})$, $\exists \displaystyle\prod_{k\in I,l\in J_k}x_{kl}\in \displaystyle\prod_{k\in I,l\in J_k}\bcP(V_{kl})$. Hence, using the \eqref{Eq-1}, and the commutativity of the diagrams we find:\\
$\pi_{ij,i'j'}\circ\rho_1(\displaystyle\prod_{k\in I,l\in J_k}x_{kl})=\pi_{ij,i'j'}\circ\rho_2(\displaystyle\prod_{k\in I,l\in J_k}x_{kl})\forall i,i'\in I,j\in J_i,j'\in J_{i'}$\\
Then, the universal property of $\displaystyle\prod_{k,k'\in I,l\in J_k,l'\in J_{k'}}\bcP(V_{kl}\times_U V_{k'l'})$ implies that: $\rho_1(\displaystyle\prod_{k\in I,l\in J_k}x_{kl})=\rho_2(\displaystyle\prod_{k\in I,l\in J_k}x_{kl})$. Hence, $\displaystyle\prod_{k\in I,l\in J_k}x_{kl}\in \bcP_U(\bcV)$. Then, the commutativity of the diagrams, and having $\ker_{\bcP,\bcV_i}$ being monomorphism $\forall i\in I$, implies that ${\bcP_{U_i}(\phi_{i,id})\circ \bcP_{f_i}(\bcV)}(\displaystyle\prod_{k\in I,l\in J_k}x_{kl})=x_i,\forall i\in I$. Therefore, $\exists x_{\bcV}=[\displaystyle\prod_{k\in I,l\in J_k}x_{kl}]\in \bcP^+(U)$ such that $\bcP^+(f_i)(x_{\bcV})=x_{\bcV_i},\forall i\in I$. I.e., $\rho(x_{\bcV})=x$\\
Then, $Ker(\rho_1,\rho_2)\subseteq\Imm(\rho)$. Hence, $Ker(\rho_1,\rho_2)=\Imm(\rho)$ and $\bcP^+$ is a sheaf.
\end{proof}
\begin{remark}
Having $\bcP$ a separated pre-sheaf implies that $i_{\bcV_i\times_U\bcV_{i'}}$ is a monomorphism, which allows using the covering the $\bcV_i\times_U\bcV_{i'}$. Otherwise, the equality \eqref{Eq-1} would have been true on a common refinement of $p_1^{\ast}\bcV_{i}$ and $p_2^{\ast}\bcV_{i'}$, with elements not necessary of the form $V_{ij}\times_U V_{i'j'}$. Then, one will not necessary be able to use the definition of $\ker_{\bcP,\bcV}$ to get, in a canonical way, an element in $\bcP_U(\bcV)$, and hence, in $\bcP^+(U)$.
\end{remark}
\begin{counterexample}
http://mathoverflow.net/questions/95579/sheafification-why-does-twice-suffice\\
http://mathoverflow.net/questions/616/what-is-an-example-of-a-presheaf-p-where-p-is-not-a-sheaf-only-a-separated-pre\\
http://math.stackexchange.com/questions/53709/sheafification-and-the-unique-decomposition-of-morphisms\\
http://math.stackexchange.com/questions/249961/sheafification-of-the-constant-presheaf\\
http://math.stackexchange.com/questions/153287/is-sheafification-always-an-inclusion\\
http://math.stackexchange.com/questions/153287/is-sheafification-always-an-inclusion\\
http://mathoverflow.net/questions/95579/sheafification-why-does-twice-suffice
\end{counterexample}
\begin{proof}
!!!
\end{proof}
\begin{lemma}
The functor $-^+:\PreC\rightarrow \PreC$ is left exact.
\end{lemma}
\begin{proof}
!!! Tamme P 38
\end{proof}
\begin{remark}
Since $-^+$ is left exact, it preserves the kernel, product and limits. But $-^+$ is not right exact. Hence, it does not necessary preserve cokernel, image, coimage, coproduct or colimits.
\end{remark}
\tcb{sheafification of zero and constant pre-sheaves}

\begin{lemma}
There exist a \tcb{unique} morphism of pre-sheave $\varphi^+:\bcP^+\\rightarrow \bcQ^+$ that makes $+:\PreC\rightarrow \PreC$ a functor, and the following diagram commutative:
$$
\xymatrix{\bcP\ar[d]_{\eta}\ar[r]^{\varphi}&\bcQ\ar[d]^{\eta}\\
\bcP^+\ar@{-->}[r]_{\varphi^+} &\bcQ^+
}
$$
\end{lemma}
\begin{proof}
\tcg{Don't bother with i if it doesn't add additional information, that the adjunction is guaranteed by the universal property.}
\end{proof}
\begin{definition}[Associated sheaf]
Define $-^{\hat{+}}:(-^+)^+:\PreC\rightarrow \PreC$.
\end{definition}

\begin{lemma}
If $\bcP$ is a sheaf, then $\eta:\bcP\rightarrow \bcP^+$ is an isomorphism
\end{lemma}
\begin{proof}
Let $\bcP$ be a sheaf, then $\forall U\in oc(\bcC), \forall \bcU\in \Cov(U)$. Then, $\eta_{\bcU}$ is an isomorphism. Hence, $\forall (\epsilon, \phi):\bcU'\rightarrow \bcU $ in $\Cov(U)$, we have $\bcP_U((\epsilon, \phi))=\eta_{\bcU'}\circ \eta^{-1}_{\bcU}$ which is an isomorphism. Hence, $\bcP^+(U)=\Colim_{\Cov^{op}(U)}\bcP_U$ is isomorphic to $\bcP_U(\bcU)\forall \bcU\in \Cov(U)$, i.e. $i_{\bcU}$ is an isomorphism $\forall \bcU\in \Cov(U)$. Hence, $\eta_U$ is an isomorphism $\forall U\in \bcC$, i.e. $\eta$ is an isomorphism.\\
\tcr{Or, we could have used that fact that the (co)limit of isomorphisms is an isomorphism.}
\end{proof}
\begin{lemma}\label{UniqueFactorise-1}
Let $\varphi:\bcP\rightarrow \bcQ$ be an arrow of pre-sheaves. Where, $\bcQ$ is a sheaf \tcb{would separated pre-sheaf work?}. Then, $\varphi$ factorise uniquely through $\eta_{\bcP}$.
\end{lemma}
\begin{proof}
Using the definition of $\varphi^+$, the following diagram commutes:
$$
\xymatrix{
\bcP\ar[r]^{\eta_{\bcP}}\ar[d]_{\varphi}&\bcP^+\ar[d]^{\varphi^+}\\
\bcQ\ar[r]_{\eta_{\bcQ}}&\bcQ^+
}
$$
Since, $\bcQ$ is a sheaf, then $\eta_{\bcQ}$ is an isomorphism. Hence, $\varphi=(\eta^{-1}_{\bcQ}\circ \varphi^+ )\circ \eta_{\bcP}$.\\
Assume that there is $\zeta\bcP^+\rightarrow \bcQ$ such that $\varphi=\zeta\circ \eta_{\bcP}$. Then, consider the diagram:
$$
\xymatrix{
\bcP\ar[r]^{\eta_{\bcP}}\ar[d]_{\varphi}&\bcP^+\ar[d]^{\varphi^+}\ar[ld]|{\zeta}\\
\bcQ\ar[r]_{\eta_{\bcQ}}&\bcQ^+
}
$$
\tcg{finish prove}



\end{proof}
\begin{lemma}\label{UniqueFactorise-2}
Let $\varphi:\bcP\rightarrow \bcQ$ be an arrow of pre-sheaves. Where, $\bcQ$ is a sheaf . Then, $\varphi$ factorises uniquely through $\hat{\eta}_{\bcP}:=\eta_{\bcP}\circ \eta_{\bcP}$.
\end{lemma}
\begin{proof}
Consider the following commutative diagram
$$
\xymatrix{
\bcP\ar[r]^{\eta_{\bcP}}\ar[d]_{\varphi}&\bcP^+\ar[r]^{\eta_{\bcP^+}}\ar[d]_{\varphi^+}&\bcP^{\hat{+}}\ar[d]^{\varphi^{\hat{+}}}\\
\bcQ\ar[r]_{\eta_{\bcQ}}&\bcQ^+\ar[r]_{\eta_{\bcQ^+}}&\bcQ^{\hat{+}}
}
$$
The commutativity of the above diagram is due to the definition of $\varphi^+$ and $\varphi^{\hat{+}}$.\\
Since, $\bcQ$ is a sheaf, then $\eta_{\bcQ}$ is an isomorphism. Having $\bcQ$ a sheaf implies also that $\bcQ^+$ is a sheaf, then $\eta_{\bcQ^+}$ is an isomorphism. Hence, $\varphi$ factorises as $\varphi=(\hat{\eta}^{-1}_{\bcQ}\circ \varphi^{\hat{+}} )\circ \hat{\eta}_{\bcP}$.\\
Assume that there is $\zeta:\bcP^{\hat{+}}\rightarrow \bcQ$ such that $\varphi=\zeta\circ \hat{\eta}_{\bcP}$. Then, consider the diagram:
$$
\xymatrix{
\bcP\ar[r]^{\eta_{\bcP}}\ar[d]_{\varphi}&\bcP^+\ar[r]^{\eta_{\bcP^+}}\ar[d]_{\varphi^+}&\bcP^{\hat{+}}\ar[d]^{\varphi^{\hat{+}}}\ar[lld]|{\zeta}\\
\bcQ\ar[r]_{\eta_{\bcQ}}&\bcQ^+\ar[r]_{\eta_{\bcQ^+}}&\bcQ^{\hat{+}}
}
$$
Since, $\varphi=\zeta\circ \hat{\eta}_{\bcP}$ then the following diagram commute:
$$
\xymatrix{
\bcP\ar[r]^{\eta_{\bcP}}\ar[d]_{\varphi}&\bcP^+\ar[d]^{\eta_{\bcQ} \circ\zeta\circ \eta_{\bcP^+}}\\
\bcQ\ar[r]_{\eta_{\bcQ}}&\bcQ^+
}
$$
Then, \ref{UniqueFactorise-1} implies that $\eta_{\bcQ} \circ\zeta\circ \eta_{\bcP^+}=\varphi^+$. Hence, the following diagram commutes:
$$
\xymatrix{
\bcP^+\ar[r]^{\hat{\eta}_{\bcP}}\ar[d]_{\varphi^+}&\bcP^{\hat{+}}\ar[d]^{\hat{\eta}_{\bcQ} \circ\zeta}\\
\bcQ^+\ar[r]_{\hat{\eta}_{\bcQ}}&\bcQ^{\hat{+}}
}
$$
Then, \ref{UniqueFactorise-1} implies that $\hat{\eta}_{\bcQ} \circ\zeta=\varphi^{\hat{+}}$. Hence, $\zeta=\hat{\eta}^{-1}_{\bcQ} \circ\varphi^{\hat{+}}$. I.e. $\varphi$ factorises uniquely through $\hat{\eta}_{\bcP}$ as $\varphi=(\hat{\eta}^{-1}_{\bcQ}\circ \varphi^{\hat{+}} )\circ \hat{\eta}_{\bcP}$.
\end{proof}
\begin{proposition}\label{UniversalProperty}
There is a initial universal arrow from $\bcP$ to $\goi:\ShvC\rightarrow \PreC$
\end{proposition}
\begin{proof} $\exists \hat{\eta}_{\bcP}$, defined above, for which, \ref{UniqueFactorise-2} shows that for any $\bcQ$ in $\ShvC$ and $\varphi:\bcP\rightarrow \goi(\bcQ)$ in $\PreC$, $\exists! \zeta=\hat{\eta}^{-1}_{\bcQ} \circ\varphi^{\hat{+}}:\bcP^{\hat{+}}\rightarrow \bcQ$ in  $\ShvC$ such that the following diagram commutes:
$$
\xymatrix{\bcP\ar[rr]^{\hat{\eta}_{\bcP}}\ar[ddrr]_{\varphi}&&\goi(\bcP^{\hat{+}})=\bcP^{\hat{+}}\ar[dd]_{\goi(\zeta)}|=^{\zeta}\\
\\
&&\goi(\bcQ)=\bcQ
}
$$
\end{proof}

\begin{theorem}
$\goi$ admits left adjoint $\goi_{ad}:\PreC\rightarrow \ShvC$.
\end{theorem}
\begin{proof}
\ref{UniversalProperty} implies that $\goi$ has a left adjoint $\goi_{ad}:\PreC\rightarrow \ShvC$ such that $\forall \varphi:\bcP\rightarrow \bcQ$ in $\PreC$, $\goi_{ad}(\bcP)=\bcP^{\hat{+}}$ and $\goi_{ad}(\varphi)=\varphi^{\hat{+}}$
\end{proof}
\tcb{check preserving limits with the home functor to see it's $\goi_{ad}$ or $\goi^{ad}$}


\tcb{left adjoints preserves the limits} Use it later on\\
\tcb{right adjoints preserves the colimits}


\subsection{Category of Abelian Sheaves on a site}
\begin{theorem}
Let $\bcC_{\tau}$ be a site, $\bcA$ be an abelian category, then $\ShvC$ is an abelian category.
\end{theorem}
\begin{proof}$\ShvC$ is an additive category that:
\begin{itemize}
\item The category $\ShvC$ is a full subcategory of $\PreC$. Hence, $\forall S,T\in \ShvC$, then $S,T\in \PreC$ and $Hom_{\ShvC}(S,T)=Hom_{\PreC}(S,T)$. Then, $Hom_{\ShvC}(S,T)$ have the structure of the abelian group $Hom_{\PreC}(S,T)$, and for each morphism $\varphi: S\rightarrow T$ in $\ShvC$, $\varphi_{\ast_{\ShvC}}=\varphi_{\ast_{\PreC}}$, and $\varphi^{\ast_{\ShvC}}=\varphi^{\ast_{\PreC}}$ are group homomorphisms.
\item [*]The constant pre-sheaf $\mathbf{0}$ is evidently a sheaf. And $\forall S \in \ShvC$, $Hom_{\ShvC}(S,\mathbf{0})=Hom_{\PreC}(S,\mathbf{0})$ and $Hom_{\ShvC}(\mathbf{0},S)=Hom_{\PreC}(\mathbf{0},S)$. Hence, the zero object exist in $\ShvC$, namely $\mathbf{0}$.
\item $\ShvC$ has biproduct that: $\forall S_1,S_2 \in \ShvC$, then $S_1,S_2 \in \PreC$, and there exist $S_1\oplus S_2$ in $\PreC$. I.e. there are, \tcg{not necessary unique}, morphisms of pre-sheaves:
$$
\xymatrix{S_1\ar@<-2pt>[r]_{i_1}&S_1\oplus S_2  \ar@<-2pt>[r]_{p_2} \ar@<-2pt>[l]_{p_1}  & S_1\ar@<-2pt>[l]_{i_2}}
$$
such that\\
$p_1\circ i_1=id_{S_1}$, $p_2\circ i_2=id_{S_2}$, $p_2\circ i_1=p_1\circ i_2=0$, and $i_1\circ p_1+i_2\circ p_2=id_{S_1\oplus S_2}$.\\
%Then, consider the following diagram in $\ShvC$:$$\xymatrix{S_1\ar@<-2pt>[r]_{\hat{\eta}_{S_1}}&S^{\hat{+}}_1\ar@<-2pt>[r]_{i^{\hat{+}}_1}\ar@<-2pt>[l]_{\hat{\eta}^{-1}_{S_1}}&S_1\hat{\oplus}S_2  \ar@<+2pt>[r]^{p^{\hat{+}}_2} \ar@<-2pt>[l]_{p^{\hat{+}}_1}  & S^{\hat{+}}_2\ar@<+2pt>[l]^{i^{\hat{+}}_2}\ar@<+2pt>[r]^{\hat{\eta}^{-1}_{S_2}}&S_2\ar@<+2pt>[l]^{\hat{\eta}_{S_2}}}$$
%Where $S_1\hat{\oplus}S_2:=\goi_{ad}(S_1\oplus S_2)$. Let $\hat{p}_j=\hat{\eta}^{-1}_{S_j}\circ p^{\hat{+}}_j$, and $\hat{i}_j=i^{\hat{+}}_j\circ \hat{\eta}_{S_j}$, for $j=1,2$. Then, we have the following diagram in $\ShvC$$$\xymatrix{S_1\ar@<-2pt>[r]_{\hat{i}_1}&S_1\hat{\oplus}S_2  \ar@<+2pt>[r]^{\hat{p}_2} \ar@<-2pt>[l]_{\hat{p}_1}  & S_2\ar@<+2pt>[l]^{\hat{i}_2}}$$
%Such that, for $j=1,2$ and $(k,l)\in \{(1,2),(2,1)\}$:\\$\hat{p}_j\circ \hat{i}_j=\hat{\eta}^{-1}_{S_j}\circ p^{\hat{+}}_j \circ i^{\hat{+}}_j\circ \hat{\eta}_{S_j}=\hat{\eta}^{-1}_{S_j}\circ   (p_j\circ i_j)^{\hat{+}}  \circ \hat{\eta}_{S_j}=\hat{\eta}^{-1}_{S_j}\circ   (id_{S_j})^{\hat{+}}  \circ \hat{\eta}_{S_j}=id_{S_j}$.\\$\hat{p}_k\circ \hat{i}_l=\hat{\eta}^{-1}_{S_k}\circ p^{\hat{+}}_k \circ i^{\hat{+}}_l\circ \hat{\eta}_{S_l}=\hat{\eta}^{-1}_{S_k}\circ   (p_k\circ i_l)^{\hat{+}}  \circ \hat{\eta}_{S_l}=\hat{\eta}^{-1}_{S_k}\circ   (0)^{\hat{+}}  \circ \hat{\eta}_{S_l}=0$.\\$\hat{i}_1\circ \hat{p}_1+\hat{i}_2\circ \hat{p}_2=i^{\hat{+}}_1\circ \hat{\eta}_{S_1}\circ \hat{\eta}^{-1}_{S_1}\circ p^{\hat{+}}_1 +i^{\hat{+}}_2\circ \hat{\eta}_{S_2}\circ \hat{\eta}^{-1}_{S_2}\circ p^{\hat{+}}_2 =i^{\hat{+}}_1\circ p^{\hat{+}}_1 +i^{\hat{+}}_2\circ p^{\hat{+}}_2=(i_1\circ p_1)^{\hat{+}} +(i_2\circ p_2)^{\hat{+}} =(i_1\circ p_1 + i_2\circ p_2)^{\hat{+}}=id^{\hat{+}}_{S_1\oplus S_2}=id_{S_1\hat{\oplus}S_2}$.\\
First, we will show that $S_1\oplus S_2$ is a sheaf, then it is the direct sum of $S_1$ and $S_2$ in $\ShvC$.\\
$\forall U\in \bcC, \bcU=\{f_i:U_i\rightarrow U| i\in I \}\in \Cov(U)$, since $p_1$ and $p_2$ are morphisms of pre-sheaves, i.e. natural transformations then the below diagram commutes:
$${\tiny
\xymatrix{
0\ar[r]&S_1(U\ar@{^(->}[r]|{\rho_{S_1}})&\displaystyle\prod_{k\in I}S_1(U_k)\ar@<+2pt>[r]^{\rho_{1,S_1}}\ar@<-2pt>[r]_{\rho_{2,S_1}}&\displaystyle\prod_{k,k'\in I}S_1(U_k\times_U U_{k'})\\
0\ar[r]&(S_1\oplus S_2)(U)\ar[r]|{\rho}\ar[u]|{p_{1_U}}\ar[d]|{p_{2_U}}&\displaystyle\prod_{k\in I}(S_1\oplus S_2)(U_k)\ar@<+2pt>[r]^{\rho_1}\ar@<-2pt>[r]_{\rho_2}\ar[u]|{\displaystyle\prod_{k\in I}p_{1_{U_k}}}\ar[d]|{\displaystyle\prod_{k\in I}p_{2_{U_k}}}&\displaystyle\prod_{k,k'\in I}(S_1\oplus S_2)(U_k\times_U U_{k'})\ar[u]|{\displaystyle\prod_{k,k'\in I}p_{1_{U_k\times_U U_{k'}}}}\ar[d]|{\displaystyle\prod_{k,k'\in I}p_{2_{U_k\times_U U_{k'}}}}\\
0\ar[r]&S_2(U\ar@{^(->}[r]|{\rho_{S_2}})&\displaystyle\prod_{k\in I}S_2(U_k)\ar@<+2pt>[r]^{\rho_{1,S_2}}\ar@<-2pt>[r]_{\rho_{2,S_2}}&\displaystyle\prod_{k,k'\in I}S_2(U_k\times_U U_{k'})
}}
$$
Since the above diagram commutes and the first and last row are exact, then by \ref{3times3_2}, the middle row is exact and $S_1\oplus S_2$ is a sheaf.
\tcg{define product diagram in general}\\
$\ShvC$ is a fullsubcategory of $\PreC$, hence, $p_1,p_2, i_1$ and $i_2$ are in $\ShvC$. Therefore, there exist a direct sum $S_1\oplus S_2$ of $S_1$ and $S_2$ in $\ShvC$.\\
\item (Kernel) Let $\varphi:S\rightarrow T$ in $\ShvC$, then $\varphi$ is in $\PreC$. Hence, $K:=\Ker_{\PreC}(\varphi)$ exist in $\PreC$. We will see that $K$ is a sheaf and that it is the kernel of $\varphi$ in $\ShvC$.\\
Let $k:=\ker_{\PreC}(\varphi)$ Then, $\forall U \in \bcC, \bcU=\{U_i|i\in I\}\in \Cov(U)$, consider the commutative diagram in $\PreC$:
$$
\xymatrix{
K(U)\ar[rr]|{\rho_{K}}\ar@{^(->}[dd]_{k_U}&&\displaystyle\prod_{k\in I}K(U_k)\ar@<+2pt>[rr]^{\rho_{1,K}}\ar@<-2pt>[rr]_{\rho_{2,K}}  \ar@{^(->}[dd]|{\displaystyle\prod_{k\in I}k_{U_k}} &&\displaystyle\prod_{k,k'\in I}K(U_k\times_U U_{k'}) \ar@{^(->}[dd]|{\displaystyle\prod_{k,k'\in I}k_{U_k\times_U U_{k'}}}\\
\\
S(U)\ar@{^(->}[rr]|{\rho_{S}}\ar[dd]_{{\varphi_U}}&&\displaystyle\prod_{k\in I}S(U_k)\ar@<+2pt>[rr]^{\rho_{1,S}}\ar@<-2pt>[rr]_{\rho_{2,S}}  \ar[dd]|{\displaystyle\prod_{k\in I}{\varphi_{U_k}}} &&\displaystyle\prod_{k,k'\in I}S(U_k\times_U U_{k'}) \ar[dd]|{\displaystyle\prod_{k,k'\in I}{\varphi_{U_k\times_U U_{k'}}}}\\
\\
T(U)\ar@{^(->}[rr]|{\rho_{T}}&&\displaystyle\prod_{k\in I}T(U_k)\ar@<+2pt>[rr]^{\rho_{1,T}}\ar@<-2pt>[rr]_{\rho_{2,T}}&&\displaystyle\prod_{k,k'\in I}T(U_k\times_U U_{k'})
}
$$
Notice that the columns and second and third rows of the diagram are exact, then by \ref{3x3Diagram}, the first row is exact. Hence, $K$ is a sheaf.\\
Since $\ShvC$ is a full subcategory of $\PreC$, then $k$ in $\ShvC$, and $\varphi\circ k=0$.\\
Since $K$ is the kernel of $\varphi:S\rightarrow T$. Then, by \ref{LeftExactInverse}, we have the following exact sequence in $\Ab$, $\forall \bcX \in \PreC$:
$${\small \xymatrix{0\ar[r]&Hom_{\PreC}(\bcX,K)\ar@{^(->}[rr]^{k_{\ast}} &&Hom_{\PreC}(\bcX,S)\ar[rr]^{\varphi_{\PreC\ast}}&&Hom_{\PreC}(\bcX,T)}}
$$
Since, $\ShvC$ is a full subcategory of $\PreC$, then, in particular, the following sequence is exact in $\Ab$, $\forall \bcX \in \ShvC$:
$${\small \xymatrix{0\ar[r]&Hom_{\ShvC}(\bcX,K)\ar@{^(->}[rr]^{k_{\ast}} &&Hom_{\ShvC}(\bcX,S)\ar[rr]^{\varphi_{\PreC\ast}}&&Hom_{\ShvC}(\bcX,T)}}
$$
Since, $\ShvC$ is additive category, then, by \ref{LeftExactInverse}, the sequence $0\rightarrow K\stackrel{k}{\hookrightarrow} S \stackrel{\varphi}{\rightarrow} T$ is exact in $\ShvC$, and there exists $(K,k')$ a kernel of $\varphi:S\rightarrow T$ in $\ShvC$.\\
\tcb{Go for more efficeint proof using the fact that $\goi_{ad}$ is a left adjoint functor}
\item (Cokernel) Let $\varphi:S\rightarrow T$ in $\ShvC$, then $\varphi$ is in $\PreC$. Hence, $C:=\Coker_{\PreC}(\varphi)$ exist in $\PreC$. $C$ is not necessary a sheaf, counter example \ref{CoKerCounterEx}. Therefore, we consider its associated sheaf $C^{\hat{+}}$. Then, we will show that $C^{\hat{+}}$ is the cokernel of $\varphi$. Since $ad:\goi_{ad}\vdash\goi:\PreC\rightarrow\ShvC$. Then we have the following commutative diagram $\forall X \in \ShvC$:
$$
{\small \xymatrix{
0\ar[r]&Hom_{\PreC}(C,X)\ar@{^(->}[rr]^{c^{\ast}}&&Hom_{\PreC}(T,X)\ar[rr]^{\varphi^{\ast}}&&Hom_{\PreC}(S,X)\\
0\ar[r]&Hom_{\ShvC}(C^{\hat{+}},X)\ar[rr]^{(c^{\hat{+}})^{\ast}}\ar[u]^{ad_{C,X}}_{\cong}&&Hom_{\ShvC}(T^{\hat{+}},X)\ar[rr]^{(\varphi^{\hat{+}})^{\ast}}\ar[u]^{ad_{T,X}}_{\cong}&&Hom_{\ShvC}(S^{\hat{+}},X)\ar[u]^{ad_{S,X}}_{\cong}\\
}}
$$
The first row is exact, then by \ref{2x3Diagram}, the second row is exact. Then, by \ref{LefttExactInverse2}, we find that $\xymatrix{S^{\hat{+}}\ar[r]^{\varphi^{\hat{+}}}&T^{\hat{+}}\ar@{->>}[r]^{c^{\hat{+}}}&C^{\hat{+}}\ar[r]&0 }$ is exact.\\
Then, we will show that $C^{\hat{+}}$, along with $c':=c^{\hat{+}}\circ \hat{\eta}_T$, is a cokernel of $\varphi$. Consider the commutative diagram in $\ShvC$:
$$\xymatrix{
S^{\hat{+}}\ar[r]^{\varphi^{\hat{+}}}&T^{\hat{+}}\ar@{->>}[r]^{c^{\hat{+}}}&C^{\hat{+}}\ar[r]\ar@{-->}[d]^{h'} &0\\
S\ar[r]_{\varphi}\ar[u]^{\hat{\eta}_S}_{\cong}&T\ar@{->>}[ur]_{c'}\ar[u]^{\hat{\eta}_T}_{\cong}\ar@{..>}[r]_h&Z
}$$
Then, the commutativity of the diagram implies that $c'\circ \varphi=(c^{\hat{+}}\circ \varphi^{\hat{+}})\circ \hat{\eta}_S=0$.
Also, let $h:T\rightarrow Z$ in $\ShvC$, such that $h\circ \varphi=0$. Then, $(h\circ \hat{\eta}_T^{-1}) \varphi^{\hat{+}}=0$. Then, the exactness of the first arrow implies that $\exists! h':C^{\hat{+}}\rightarrow Z$ such that $h\circ \hat{\eta}_T^{-1}=h'\circ c^{\hat{+}}\Rightarrow h=h'\circ (c^{\hat{+}}\circ \hat{\eta}_T)=h'\circ c'$. Then the sequence $$\xymatrix{S\ar[r]^{\varphi}&T\ar@{->>}[r]^{c'}&C^{\hat{+}}\ar[r]&0 }$$ is exact in $\ShvC$, and there exist $(C^{\hat{+}},c')$ a cokernel of $\varphi:S\rightarrow T$ in $\ShvC$.\\
\tcg{move last bit of the proof to diagram lemmas}
\item (Isomorphism) Let $\varphi:S\rightarrow T$ in $\ShvC$, then $\varphi$ is in $\PreC$. Using the settings of the previous step, $(C^{\hat{+}},c')$ is the cokernel of $\varphi$ in $\ShvC$. Since, $\ShvC$ has kernels, then $\Im_{\ShvC} \varphi\cong\Ker_{\ShvC} c'\cong\Ker_{\PreC} c'\cong \Ker_{\PreC} c^{\hat{+}}$ that $\hat{\eta}$ is a natural isomorphism. Then, since $\goi_{ad}$ \tcb{preserves the limits for being left adjoint}, then $\Im_{\ShvC} \varphi\cong (\Ker \coker \varphi)^{\hat{+}}=(\Im_{\PreC} \varphi)^{\hat{+}}$. Then, let $J:\Coim_{\PreC} \varphi$ and $I:=\Im_{\PreC} \varphi$. Then, having $\PreC$ an abelain category implies that the canonical morphism \eqref{} $\tilde{\varphi}:J\rightarrow$ is an isomorphism, and that the following diagram commutes:
$$
\xymatrix{S\ar[rrr]^{\varphi}\ar[dr]_{j}&&&T\\
&J\ar[r]_{\tilde{\varphi}^{\hat{+}}}&I\ar[ru]_{i}
}
$$
Then, $\tilde{\varphi}^{\hat{+}}$ is an isomorphism. And $J^{\hat{+}}\cong(\Coker_{\PreC} \ker_{\PreC} \varphi)^{\hat{+}}\cong(\Coker_{\PreC} \ker_{\ShvC} \varphi)^{\hat{+}}=(\Coker_{\ShvC} \ker_{\ShvC} \varphi)=\Coim_{\ShvC} \varphi$, and the folloing diagram commutes:
$$
\xymatrix{S\ar[rrr]^{\varphi=\hat{\eta}_T^{-1}\circ \varphi\circ \hat{\eta}_S}\ar[dr]_{j^{\hat{+}}\circ \hat{\eta}_S}&&&T\\
&J^{\hat{+}}\ar[r]_{\tilde{\varphi}^{\hat{+}}}&I^{\hat{+}}\ar[ru]_{\hat{\eta}_T^{-1}\circ  i^{\hat{+}}}&
}
$$
\tcg{Explain the isomorphisms}
\end{itemize}
\end{proof}
\begin{counterexample}[Finite Coproduct]
Let $S_1,S_2\in \ShvC$, then $S_1\oplus S_2$ in $\PreC$ is not necessary a sheaf:\\
\tcg{Finish the example}
\end{counterexample}
\begin{counterexample}\label{CoKerCounterEx}
Cokernel counter example
\tcg{Finish the example}
\end{counterexample}
\black 